u_iInf₂ — Mathlib

English

Let α and β be complete lattices and l,u form a Galois connection. For a family f: ∀ i, κ(i) → β, we have u( inf_{i} inf_{j} f(i,j) ) = inf_{i,j} u( f(i,j) ). This extends the single-index preservation to a two-parameter family.

Русский

Пусть α и β — полные решетки и связь Галуа между ними. Для семейства f: ∀ i, κ(i) → β выполняется: u( inf_{i} inf_{j} f(i,j) ) = inf_{i,j} u( f(i,j) ).

LaTeX

$$$$ u\\Big( \\inf_{i} \\inf_{j} f(i,j) \\Big) = \\inf_{i,j} u(f(i,j)). $$$$

Lean4

theorem u_iInf₂ {f : ∀ i, κ i → β} : u (⨅ (i) (j), f i j) = ⨅ (i) (j), u (f i j) :=
  gc.dual.l_iSup₂

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