English
A bi-Sup version: for any predicate p and families f,g defined on indices with p, the symmetric difference of the two biSups is bounded by the biSups of the pointwise symmetric differences.
Русский
Би-Sup версия: для предиката p и семейств f,g по индексам с p, симметрическая разность двух би-Sup ограничена би-Sup точечных симмDiff.
LaTeX
$$${p} \Rightarrow (\text{symmDiff}(\bigvee_i\, f_i, \bigvee_i\, g_i) \le \bigvee_i\, \bigl( f_i \Delta g_i \bigr)).$$$
Lean4
/-- 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
