iInf_sum — Mathlib

English

Let f: β ⊕ γ → α. Then the infimum over all inputs equals the infimum over the left and right injections: ⨅ x, f x = ⨅ i, f (inl i) ⨅ ⨅ j, f (inr j).

Русский

Пусть f: β ⊕ γ → α. Тогда инфимум по всем входам равен инфимуму над левой и правой частями: inf_x f(x) = inf_i f(inl i) ⊓ inf_j f(inr j).

LaTeX

$$$\\displaystyle \\big\\wedge_{x} f(x) = \\big\\wedge_{i} f(\\mathrm{inl}\\, i) \\; \\wedge \\; \\big\\wedge_{j} f(\\mathrm{inr}\\, j)$$$

Lean4

theorem iInf_sum {f : β ⊕ γ → α} : ⨅ x, f x = (⨅ i, f (Sum.inl i)) ⊓ ⨅ j, f (Sum.inr j) :=
  @iSup_sum αᵒᵈ _ _ _ _

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