iInf_and' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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