map_iSup

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.map_iSup

English

Image commutes with arbitrary suprema: map f (⨆ i, L_i) = ⨆ i, map f (L_i).

Русский

Изображение сохраняет произвольную верхнюю границу: map f (⨆ i, L_i) = ⨆ i, map f (L_i).

LaTeX

$$(Sublattice.map f) (iSup i, L i) = iSup i, Sublattice.map f (L i)$$

Lean4

theorem map_iSup (f : LatticeHom α β) (L : ι → Sublattice α) : (⨆ i, L i).map f = ⨆ i, (L i).map f :=
  (gc_map_comap f).l_iSup

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru