iInf_and — Mathlib

English

Let p and q be propositions and s: (p ∧ q) → α. Then iInf over p and q of s equals ⨅_(h1) ⨅_(h2) s h1 h2.

Русский

Пусть p и q — суждения, и s: (p ∧ q) → α. Тогда iInf по p и q от s равен двум инфимумам: ⨅_{h1} ⨅_{h2} s h1 h2.

LaTeX

$$$\\\\bigwedge_{h_1} \\\\bigwedge_{h_2} s(h_1,h_2) = \\\\bigwedge_{h_1,h_2} s(h_1,h_2)$$$

Lean4

theorem iInf_and {p q : Prop} {s : p ∧ q → α} : iInf s = ⨅ (h₁) (h₂), s ⟨h₁, h₂⟩ :=
  @iSup_and αᵒᵈ _ _ _ _

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