mathlib
06886125 - feat(order/rel_iso): constructors for rel embeddings (#7046)

Commit

4 years ago

feat(order/rel_iso): constructors for rel embeddings (#7046) Alternate constructors for relation and order embeddings which require slightly less to prove.

Author

b-mehta

Parents

ea4dce03

mathlib 06886125 - feat(order/rel_iso): constructors for rel embeddings (#7046)

mathlib
06886125 - feat(order/rel_iso): constructors for rel embeddings (#7046)