English
A variant form: disjointed of an adjusted partialSups map remains equal to disjointed f.
Русский
Вариант: disjointed от модифицированной карты partialSups равен disjointed f.
LaTeX
$$$\operatorname{disjointed}(\operatorname{OrderHom.instFunLike.coe}(\operatorname{partialSups} f)) = \operatorname{disjointed} f$$$
Lean4
/-- `disjointed f` is the unique map `d : ι → α` such that `d` has the same partial sups as `f`,
and `d i` and `d j` are disjoint whenever `i < j`. -/
theorem disjointed_unique {f d : ι → α} (hdisj : ∀ {i j : ι} (_ : i < j), Disjoint (d i) (d j))
(hsups : partialSups d = partialSups f) : d = disjointed f :=
by
rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]
exact funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm
