English
The partialSups of disjointed f equal the partialSups of f.
Русский
PartialSups для disjointed f равны PartialSups для f.
LaTeX
$$$\forall f:\ partialSups(\operatorname{disjointed} f) = \operatorname{partialSups}(f).$$$
Lean4
theorem sup_disjointed [Fintype ι] (f : ι → α) : univ.sup (disjointed f) = univ.sup f := by
classical
have hun : univ.biUnion Iic = (univ : Finset ι) := by ext r;
simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, ← partialSups_apply,
partialSups_disjointed]
