Commit 2025-01-21 20:44 1d24f3cf

View on Github →

refactor(Order/Disjointed): allow arbitrary partial orders as domain (#20545)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Disjointed.lean

added def Nat.disjointedRec

added theorem disjointedRec_zero

added theorem disjointed_add_one

Modified Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

added theorem MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finite

modified theorem MeasureTheory.OuterMeasure.isCaratheodory_disjointed

modified theorem MeasureTheory.OuterMeasure.isCaratheodory_partialSups

Modified Mathlib/MeasureTheory/SetSemiring.lean

modified theorem MeasureTheory.IsSetRing.disjointed_mem

added theorem MeasureTheory.IsSetRing.finsetSup_mem

modified theorem MeasureTheory.IsSetRing.partialSups_mem

Modified Mathlib/Order/Disjointed.lean

added theorem Fintype.exists_disjointed_le

added theorem Fintype.sup_disjointed

added theorem Monotone.disjointed_succ_sup

modified theorem disjoint_disjointed

added theorem disjoint_disjointed_of_lt

modified def disjointed

added theorem disjointedRec

deleted def disjointedRec

deleted theorem disjointedRec_zero

added theorem disjointed_apply

added theorem disjointed_bot

modified theorem disjointed_eq_inf_compl

modified theorem disjointed_eq_inter_compl

added theorem disjointed_eq_self

modified theorem disjointed_le

modified theorem disjointed_le_id

added theorem disjointed_of_isMin

added theorem disjointed_partialSups

modified theorem disjointed_subset

modified theorem disjointed_succ

added theorem disjointed_unique'

modified theorem disjointed_unique

modified theorem iSup_disjointed

modified theorem iUnion_disjointed

modified theorem partialSups_disjointed

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