iSup_and' — Mathlib

English

The symmetric form of iSup_and: the supremum over h1 and h2 equals the supremum over h: p ∧ q of s(h.1,h.2).

Русский

Обратная форма iSup_and: верхняя грань по парам равна верхней грани по всем парам, образующим конъюнкцию.

LaTeX

$$$\\\\bigvee_{h_1} \\\\bigvee_{h_2} s(h_1,h_2) = \\\\bigvee_{h: p ∧ q} s(h.1,h.2)$$$

Lean4

/-- The symmetric case of `iSup_and`, useful for rewriting into a supremum over a conjunction -/
theorem iSup_and' {p q : Prop} {s : p → q → α} : ⨆ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨆ h : p ∧ q, s h.1 h.2 :=
  Eq.symm iSup_and

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