feat: add 3 lemmas linking iSup and symmDiff (#12340)

Add 3 lemmas to show that the symmetric difference of two `iSup`s/`biSup`s is less or equal to the `iSup`/`biSup` of the symmetric differences.

Mathlib/Order/CompleteBooleanAlgebra.lean

@@ -470,6 +470,20 @@ theorem compl_sSup' : (sSup s)ᶜ = sInf (HasCompl.compl '' s) :=
   compl_sSup.trans sInf_image.symm
 #align compl_Sup' compl_sSup'
 
+open scoped symmDiff in
+/-- 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 ..⟩
+
+open scoped symmDiff in
+/-- A `biSup` version of `iSup_symmDiff_iSup_le`. -/
+theorem biSup_symmDiff_biSup_le {p : ι → Prop} {f g : (i : ι) → p i → α} :
+    (⨆ i, ⨆ (h : p i), f i h) ∆ (⨆ i, ⨆ (h : p i), g i h) ≤
+    ⨆ i, ⨆ (h : p i), ((f i h) ∆ (g i h)) :=
+  le_trans iSup_symmDiff_iSup_le <|iSup_mono fun _ ↦ iSup_symmDiff_iSup_le
+
 end CompleteBooleanAlgebra
 
 /--

Mathlib/Order/SymmDiff.lean

@@ -215,6 +215,12 @@ theorem symmDiff_triangle : a ∆ c ≤ a ∆ b ⊔ b ∆ c := by
   rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
 #align symm_diff_triangle symmDiff_triangle
 
+theorem le_symmDiff_sup_right (a b : α) : a ≤ (a ∆ b) ⊔ b := by
+  convert symmDiff_triangle a b ⊥ <;> rw [symmDiff_bot]
+
+theorem le_symmDiff_sup_left (a b : α) : b ≤ (a ∆ b) ⊔ a :=
+  symmDiff_comm a b ▸ le_symmDiff_sup_right ..
+
 end GeneralizedCoheytingAlgebra
 
 section GeneralizedHeytingAlgebra