map_iInf₂ — Mathlib

English

Symmetry between duality maps yields an identity relating InfTopHom.dual.symm on id.

Русский

Симметрия дуализации даёт тождество, касающееся InfTopHom.dual.symm на тождестве.

LaTeX

$$$ \\mathrm{InfTopHom}.\\mathrm{symm}.\\mathrm{dual}(\\mathrm{id}) = \\mathrm{id} $$$

Lean4

theorem map_iInf₂ [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨅ (i) (j), g i j) = ⨅ (i) (j), f (g i j) := by
  simp_rw [map_iInf]
    -- See note [lower instance priority]

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