iInf_ite — Mathlib

English

Dual of iSup_ite: the infimum of a piecewise expression equals the minimum of the two separate infima.

Русский

Двойственность iInf_ite: инфимум по разбиению на два случая равен минимальному из двух отдельных инфимумов.

LaTeX

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

Lean4

theorem iInf_ite (f g : ι → α) : ⨅ i, (if p i then f i else g i) = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), g i :=
  iInf_dite _ _ _

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