sSup_inf_sSup — Mathlib

English

In a CompletelyDistribLattice α, for any f : ∀ a, κ a → α, the iInf_iSup_eq holds: (iInf i => iSup j => f(i,j)) = (iSup g => iInf a => f(a, g(a))).

Русский

В полностью распределимой решетке справедливо: iInf_iSup_eq.

LaTeX

$$$\\inf_i \\sup_j f(i,j) = \\sup_g \\inf_i f(i, g(i))$$$

Lean4

theorem sSup_inf_sSup : sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, (p : α × α).1 ⊓ p.2 := by
  simp only [sSup_eq_iSup, biSup_inf_biSup]

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