Commit 2023-02-02 09:51 a4cb396c

View on Github →

feat: port Order.Ideal (#1985)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Ideal.lean

added theorem Order.Cofinal.above_mem

added theorem Order.Cofinal.le_above

added structure Order.Cofinal

added theorem Order.Ideal.IsCoatom.isMaximal

added theorem Order.Ideal.IsCoatom.isProper

added theorem Order.Ideal.IsMaximal.isCoatom

added theorem Order.Ideal.IsMaximal.is_coatom'

added theorem Order.Ideal.IsProper.ne_top

added theorem Order.Ideal.IsProper.not_mem_of_compl_mem

added theorem Order.Ideal.IsProper.not_mem_or_compl_not_mem

added theorem Order.Ideal.IsProper.top_not_mem

added theorem Order.Ideal.bot_mem

added theorem Order.Ideal.carrier_eq_coe

added theorem Order.Ideal.coe_inf

added theorem Order.Ideal.coe_infₛ

added theorem Order.Ideal.coe_sSubset_coe

added theorem Order.Ideal.coe_subset_coe

added theorem Order.Ideal.coe_sup

added theorem Order.Ideal.coe_sup_eq

added theorem Order.Ideal.coe_toLowerSet

added theorem Order.Ideal.coe_top

added theorem Order.Ideal.eq_sup_of_le_sup

added theorem Order.Ideal.ext

added theorem Order.Ideal.inter_nonempty

added theorem Order.Ideal.isMaximal_iff_isCoatom

added theorem Order.Ideal.isProper_iff_ne_top

added theorem Order.Ideal.isProper_of_ne_top

added theorem Order.Ideal.isProper_of_not_mem

added theorem Order.Ideal.lt_sup_principal_of_not_mem

added theorem Order.Ideal.mem_compl_of_ge

added theorem Order.Ideal.mem_inf

added theorem Order.Ideal.mem_infₛ

added theorem Order.Ideal.mem_of_mem_of_le

added theorem Order.Ideal.mem_principal

added theorem Order.Ideal.mem_sup

added def Order.Ideal.principal

added theorem Order.Ideal.principal_bot

added theorem Order.Ideal.principal_le_iff

added theorem Order.Ideal.principal_top

added theorem Order.Ideal.sup_mem

added theorem Order.Ideal.sup_mem_iff

added theorem Order.Ideal.toLowerSet_injective

added theorem Order.Ideal.top_of_top_mem

added theorem Order.Ideal.top_toLowerSet

added structure Order.Ideal

added def Order.IsIdeal.toIdeal

added structure Order.IsIdeal

added theorem Order.cofinal_meets_idealOfCofinals

added def Order.idealOfCofinals

added theorem Order.mem_idealOfCofinals

added theorem Order.sequenceOfCofinals.encode_mem

added theorem Order.sequenceOfCofinals.monotone