iInf_or — Mathlib

English

Let p and q be propositions and s: Or p q → α. Then iInf over x equals the infimum of iInf over i with s(Or.inl i) and iInf over j with s(Or.inr j).

Русский

Пусть p и q — суждения, и s: Or p q → α. Тогда iInf по x равен инфимуму по Or.inl и Or.inr.

LaTeX

$$$\\\\bigwedge_{x} s(x) = (\\\\bigwedge_i s(Or.inl i)) \\\\wedge (\\\\bigwedge_j s(Or.inr j))$$$

Lean4

theorem iInf_or {p q : Prop} {s : p ∨ q → α} : ⨅ x, s x = (⨅ i, s (Or.inl i)) ⊓ ⨅ j, s (Or.inr j) :=
  @iSup_or αᵒᵈ _ _ _ _

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