Commit 2023-01-29 16:50 dff1bd64

View on Github →

feat: port Order.Disjointed (#1920)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Disjointed.lean

added theorem Monotone.disjointed_eq

added theorem disjoint_disjointed

added def disjointed

added def disjointedRec

added theorem disjointedRec_zero

added theorem disjointed_eq_inf_compl

added theorem disjointed_eq_inter_compl

added theorem disjointed_le

added theorem disjointed_le_id

added theorem disjointed_subset

added theorem disjointed_succ

added theorem disjointed_unique

added theorem disjointed_zero

added theorem partialSups_disjointed

added theorem preimage_find_eq_disjointed

added theorem supᵢ_disjointed

added theorem unionᵢ_disjointed