map_iInf — Mathlib

English

A Inf-preserving morphism commutes with arbitrary infima: f(∧ i g(i)) = ∧ i f(g(i)).

Русский

Гомоморфизм, сохраняющий инфимы, сохраняет произвольные инфимы: f(∧ i g(i)) = ∧ i f(g(i)).

LaTeX

$$$ f\\left( \\big\\wedge_i g(i) \\right) = \\big\\wedge_i f(g(i)) $$$

Lean4

@[simp]
theorem map_iInf [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α) : f (⨅ i, g i) = ⨅ i, f (g i) := by
  simp [iInf, ← Set.range_comp, Function.comp_def]

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