Commit 2026-09-07 14:31 9122aca6

View on Github →

chore(Order/Irreducible): use to_dual (#43336) This PR uses to_dual on SupIrred/InfIrred and SupPrime/InfPrime.

Estimated changes

Modified Mathlib/Order/Birkhoff.lean

modified theorem LowerSet.supIrred_Iic

modified theorem LowerSet.supIrred_iff_of_finite

deleted def OrderEmbedding.infIrredUpperSet

deleted theorem OrderEmbedding.infIrredUpperSet_apply

deleted theorem OrderEmbedding.infIrredUpperSet_surjective

modified theorem OrderEmbedding.supIrredLowerSet_apply

deleted theorem OrderIso.infIrredUpperSet_apply

deleted theorem OrderIso.infIrredUpperSet_symm_apply

modified theorem OrderIso.supIrredLowerSet_apply

modified theorem OrderIso.supIrredLowerSet_symm_apply

deleted theorem UpperSet.infIrred_Ici

deleted theorem UpperSet.infIrred_iff_of_finite

Modified Mathlib/Order/Interval/Finset/Basic.lean

deleted theorem Finset.inf_Ici

modified theorem Finset.sup_Iic

Modified Mathlib/Order/Irreducible.lean

deleted theorem InfIrred.finset_inf_eq

deleted theorem InfIrred.ne_top

deleted def InfIrred

deleted theorem InfPrime.finset_inf_le

deleted theorem InfPrime.inf_le

deleted theorem InfPrime.ne_top

deleted def InfPrime

deleted theorem IsMax.not_infIrred

deleted theorem IsMax.not_infPrime

deleted theorem exists_infIrred_decomposition

deleted theorem infIrred_iff_not_isMax

deleted theorem infIrred_ofDual

deleted theorem infPrime_iff_infIrred

deleted theorem infPrime_iff_not_isMax

deleted theorem infPrime_ofDual

deleted theorem not_infIrred

deleted theorem not_infIrred_top

deleted theorem not_infPrime

deleted theorem not_infPrime_top

deleted theorem supIrred_toDual

deleted theorem supPrime_toDual

Modified Mathlib/Order/UpperLower/Principal.lean