map_iSup — Mathlib

English

The map sends directed suprema to suprema: the image of a supremum over an index set is the supremum of the images.

Русский

Отображение переводит направленные кумулятивные пределы в пределы: образ наибольшего по индексу равен наибольшему образов.

LaTeX

$$$ (\bigvee i, N_i).map f = \bigvee i, (N_i.map f) $$$

Lean4

@[simp]
theorem map_iSup {ι : Sort*} (N : ι → LieSubmodule R L M) : (⨆ i, N i).map f = ⨆ i, (N i).map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

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