English
Disjointed of partialSups f equals disjointed f.
Русский
Disjointed от partialSups f равен disjointed f.
LaTeX
$$$\operatorname{disjointed}(\operatorname{partialSups} f) = \operatorname{disjointed} f$$$
Lean4
theorem disjointed_partialSups (f : ι → α) : disjointed (partialSups f) = disjointed f := by
classical
ext i
have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f :=
by
rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
simp only [funext (partialSups_apply f), sup'_eq_sup]
rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
congr 2 with r
simpa only [mem_biUnion, mem_Iio, mem_Iic] using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
