comap_iInf

Mathlib.Order.Sublattice

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

English

For Sublattices L, M ⊆ β, comap f L ⊔ comap f M ≤ comap f (L ⊔ M).

Русский

Обратный образ образует верхнее объединение: comap f L ⊔ comap f M ≤ comap f (L ⊔ M).

LaTeX

$$comap f L ⊔ comap f M ≤ comap f (L ⊔ M)$$

Lean4

theorem comap_iInf (f : LatticeHom α β) (s : ι → Sublattice β) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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

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

Разделы

Аффилиация

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