iSup_and — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iSup_and {p q : Prop} {s : p ∧ q → α} : iSup s = ⨆ (h₁) (h₂), s ⟨h₁, h₂⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h) (iSup₂_le fun _ _ => le_iSup _ _)

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