map_finite_iInf — Mathlib

English

If ι is finite, then f( inf_{i} g(i) ) = inf_{i} f(g(i)) for a suitable F preserving infima.

Русский

Если индексное множество ι конечное, тогда отображение сохраняет инфимум над g.

LaTeX

$$$\text{Finite}(\iota) \Rightarrow f(\big\wedge_{i} g(i)) = \big\wedge_{i} f(g(i)).$$$

Lean4

theorem map_finite_iInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β]
    [Finite ι] (f : F) (g : ι → α) : f (⨅ i, g i) = ⨅ i, f (g i) :=
  by
  rw [← iInf_univ (f := g), ← iInf_univ (f := fun i ↦ f (g i))]
  exact map_finite_biInf finite_univ f g

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