Commit 2026-04-22 14:48 90673107

View on Github →

feat(Order/Ideal): more results on order ideals (#34820) Some iffs, closure of finite supremum, and that every proper ideal is contained in a maximal ideal.

Estimated changes

Modified Mathlib/Order/Ideal.lean

added theorem Order.Ideal.IsProper.exists_le_maximal

deleted theorem Order.Ideal.IsProper.top_notMem

added theorem Order.Ideal.biSup_finset_mem_iff

added theorem Order.Ideal.biSup_mem_iff

added theorem Order.Ideal.coe_toIdeal

added theorem Order.Ideal.exists_maximal

added theorem Order.Ideal.iSup_mem_iff

added theorem Order.Ideal.isProper_iff_top_notMem

added theorem Order.Ideal.isProper_principal_iff

added theorem Order.Ideal.le_toIdeal

added theorem Order.Ideal.mem_toIdeal

added theorem Order.Ideal.toIdeal_le

added theorem Order.Ideal.top_mem_iff_eq_top

added theorem Order.Ideal.top_notMem_iff_ne_top

deleted theorem Order.Ideal.top_of_top_mem