map_finite_iSup — Mathlib

English

If ι is finite, then for any f and g, f( sup_{i} g(i) ) equals sup_{i} f(g(i)).

Русский

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

LaTeX

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

Lean4

theorem map_finite_iSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β]
    [Finite ι] (f : F) (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i) :=
  by
  rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]
  exact map_finite_biSup finite_univ f g

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