comap_inf

Mathlib.Order.Sublattice

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

English

Comap distributes over infimum: comap f (L ⊓ M) = comap f L ⊓ comap f M.

Русский

Обратное распределяется по наименьшему: comap f (L ⊓ M) = comap f L ⊓ comap f M.

LaTeX

$$(L ⊓ M).comap f = L.comap f ⊓ M.comap f$$

Lean4

theorem comap_inf (L M : Sublattice β) (f : LatticeHom α β) : (L ⊓ M).comap f = L.comap f ⊓ M.comap f :=
  (gc_map_comap f).u_inf

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

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

Разделы

Аффилиация

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