Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 01:49 16a5286f

View on Github →

feat(order/atoms): add lemmas (#14162)

Estimated changes

deleted theorem eq_bot_or_eq_of_le_atom
deleted theorem eq_top_or_eq_of_coatom_le
added theorem is_atom.Iic_eq
added theorem is_atom.le_iff
added theorem is_atom.lt_iff
modified def is_atom
modified theorem is_atom_dual_iff_is_coatom
added theorem is_coatom.Ici_eq
added theorem is_coatom.le_iff
added theorem is_coatom.lt_iff
modified def is_coatom
modified theorem is_coatom_dual_iff_is_atom