iInf_dite — Mathlib

English

Dual of iSup_dite: infimum of a dependent if-then-else equals the infimum of two separate matters over p and ¬p.

Русский

Двойственность iInf_dite: инфимум зависимого ветвления равен инфимуму по двум случаям (p и ¬p).

LaTeX

$$$\\\\bigwedge_i \\ (if \\ h : p(i) \\ then f(i,h) \\ else g(i,h)) = \\\\min \\\\bigl( \\\\bigwedge_i \\bigl( f(i,h) \\bigr) , \\\\bigwedge_i \\bigl( g(i,h) \\bigr) \\\bigr)$$$

Lean4

theorem iInf_dite (f : ∀ i, p i → α) (g : ∀ i, ¬p i → α) :
    ⨅ i, (if h : p i then f i h else g i h) = (⨅ (i) (h : p i), f i h) ⊓ ⨅ (i) (h : ¬p i), g i h :=
  iSup_dite p (show ∀ i, p i → αᵒᵈ from f) g

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