English
The symmetric difference of two arbitrary iSup's is contained in the iSup of pairwise symmetric differences: (⊔_i f_i) Δ (⊔_i g_i) ≤ ⊔_i (f_i Δ g_i).
Русский
Симметрическая разность двух произвольных iSup'ов содержится в iSup по попарным симмDiff: (⊔_i f_i) Δ (⊔_i g_i) ≤ ⊔_i (f_i Δ g_i).
LaTeX
$$$\bigl(\bigvee_i f_i\bigr) \Delta \bigl(\bigvee_i g_i\bigr) \le \bigvee_i (f_i \Delta g_i).$$$
Lean4
/-- The symmetric difference of two `iSup`s is at most the `iSup` of the symmetric differences. -/
theorem iSup_symmDiff_iSup_le {g : ι → α} : (⨆ i, f i) ∆ (⨆ i, g i) ≤ ⨆ i, ((f i) ∆ (g i)) :=
by
simp_rw [symmDiff_le_iff, ← iSup_sup_eq]
exact
⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩
