Commit 2026-04-21 16:31 af9d0d7e

View on Github →

feat: miscellaneous results on DirSupClosed (#37670)

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

added theorem isGLB_congr_of_antisymmRel

added theorem isLUB_congr_of_antisymmRel

Modified Mathlib/Order/DirSupClosed.lean

added theorem DirSupClosed.mem_iff_of_antisymmRel

added theorem DirSupClosed.mem_imp_of_antisymmRel

added theorem DirSupClosed.of_isEmpty

added theorem DirSupClosedOn.of_isEmpty

added theorem DirSupInacc.mem_iff_of_antisymmRel

added theorem DirSupInacc.of_isEmpty

added theorem DirSupInaccOn.of_isEmpty

modified theorem IsLowerSet.dirSupInacc

added theorem IsLowerSet.dirSupInaccOn

added theorem IsUpperSet.dirSupClosedOn

added theorem PartialOrder.dirSupClosedOn_singleton

added theorem PartialOrder.dirSupClosed_singleton

added theorem dirSupClosedOn_Iic

added theorem dirSupClosedOn_iff_forall_sSup

modified theorem dirSupClosed_Iic

modified theorem dirSupClosed_iff_forall_sSup

added theorem dirSupInaccOn_Iic

added theorem dirSupInaccOn_iff_forall_sSup

added theorem dirSupInacc_Iic

modified theorem dirSupInacc_iff_forall_sSup