comap_comap

Mathlib.Order.Sublattice

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

English

Preimages along a composition equal the preimage along the composed map.

Русский

Предобразы по композиции равны предобразу по композиции.

LaTeX

$$$(L.comap g).comap f = L.comap (g \circ f)$$$

Lean4

@[simp]
theorem comap_comap (L : Sublattice γ) (g : LatticeHom β γ) (f : LatticeHom α β) :
    (L.comap g).comap f = L.comap (g.comp f) :=
  rfl

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

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

Разделы

Аффилиация

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