map_iSup — Mathlib

English

A Sup-preserving morphism commutes with arbitrary suprema: f(∨ i g(i)) = ∨ i f(g(i)).

Русский

Отображение, сохраняющее наибольшие элементы, коммутирует с произвольными верхними пределами: f(∨ i g(i)) = ∨ i f(g(i)).

LaTeX

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

Lean4

@[simp]
theorem map_iSup [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i) := by
  simp [iSup, ← Set.range_comp, Function.comp_def]

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