Commit 2024-12-10 17:02 a38f191d

View on Github →

feat: sup-closed sets are closed under finite suprema (#18990) From GrowthInGroups

Estimated changes

Modified Mathlib/Order/SupClosed.lean

added theorem InfClosed.biInf_mem

added theorem InfClosed.biInf_mem_of_nonempty

added theorem InfClosed.iInf_mem

added theorem InfClosed.iInf_mem_of_nonempty

added theorem InfClosed.sInf_mem

added theorem InfClosed.sInf_mem_of_nonempty

added theorem SupClosed.biSup_mem

added theorem SupClosed.biSup_mem_of_nonempty

added theorem SupClosed.iSup_mem

added theorem SupClosed.iSup_mem_of_nonempty

added theorem SupClosed.sSup_mem

added theorem SupClosed.sSup_mem_of_nonempty