Commit 2026-09-28 03:52 c556e0d7

View on Github →

chore(Order/Atoms): use to_dual (#43322) This PR uses to_dual for IsAtomic/IsCoatomic and IsAtomistic/IsCoatomistic.

Estimated changes

deleted theorem IsCoatom.Ici
deleted theorem IsCoatom.Ici_eq
deleted theorem IsCoatom.codisjoint_of_ne
deleted theorem IsCoatom.le_iff
deleted theorem IsCoatom.le_iff_eq
deleted theorem IsCoatom.lt_iff
deleted theorem IsCoatom.lt_top
deleted theorem IsCoatom.ne_iff_eq_top
deleted theorem IsCoatom.ne_top
deleted theorem IsCoatom.ne_top_iff_eq
deleted theorem IsCoatom.sup_eq_top_of_ne
deleted def IsCoatom
deleted theorem IsCoatomic.exists_coatom
added theorem IsSimpleOrder.mk'
deleted theorem Set.Iic.isCoatom_iff
deleted theorem covBy_iff_coatom_Iic
deleted theorem covBy_top_iff
deleted theorem eq_sInf_coatoms
added theorem eq_top_or_eq_bot
deleted theorem isAtom_dual_iff_isCoatom
deleted theorem isCoatom_bot
modified theorem isCoatom_dual_iff_isAtom
deleted theorem isCoatom_iff_eq_bot
deleted theorem isCoatom_iff_ge_of_le
deleted theorem Codisjoint.inf_left
deleted theorem Codisjoint.inf_right
deleted theorem Complementeds.coe_inf
deleted theorem Complementeds.coe_top
deleted theorem Complementeds.mk_inf_mk
deleted theorem Complementeds.mk_top
deleted theorem IsCompl.inf_sup
deleted theorem IsComplemented.inf
deleted theorem codisjoint_inf_left
deleted theorem codisjoint_inf_right
deleted theorem eq_bot_of_isCompl_top
deleted theorem eq_bot_of_top_isCompl
deleted theorem isCompl_top_bot
deleted theorem isComplemented_top