Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 03:03 5d25c8ab

View on Github →

feat(order/atoms): Galois (co)insertions and (co)atoms (#16663)

Estimated changes

Modified src/order/atoms.lean

added theorem galois_coinsertion.is_atom_iff

added theorem galois_coinsertion.is_atom_of_image

added theorem galois_coinsertion.is_coatom_iff'

added theorem galois_coinsertion.is_coatom_iff

added theorem galois_coinsertion.is_coatom_of_l_top

added theorem galois_insertion.is_atom_iff'

added theorem galois_insertion.is_atom_iff

added theorem galois_insertion.is_atom_of_u_bot

added theorem galois_insertion.is_coatom_iff

added theorem galois_insertion.is_coatom_of_image

added theorem order_embedding.is_atom_of_map_bot_of_image

added theorem order_embedding.is_coatom_of_map_top_of_image

modified theorem order_iso.is_atom_iff

modified theorem order_iso.is_atomic_iff

modified theorem order_iso.is_coatom_iff

modified theorem order_iso.is_coatomic_iff

modified theorem order_iso.is_simple_order

modified theorem order_iso.is_simple_order_iff