iSup_ite — Mathlib

English

The supremum of a pointwise ite expression equals the maximum of the two separate suprema.

Русский

Супремум по точечному выражению ite равен максимуму двух отдельных супремумов.

LaTeX

$$$\\\\bigvee_i \\\\text{ite}(p(i), f(i), g(i)) = \\\\max \\\\bigl( \\\\bigvee_i f(i), \\\\bigvee_i g(i) \\bigr)$$$

Lean4

theorem iSup_ite (f g : ι → α) : ⨆ i, (if p i then f i else g i) = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), g i :=
  iSup_dite _ _ _

Похожие утверждения