map_le_iff_le_comap

Mathlib.Order.Sublattice

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

English

For any Sublattice L ⊆ α and M ⊆ β, map f L ≤ M if and only if L ≤ comap f M.

Русский

Для любых подрешёток L ⊆ α и M ⊆ β выполняется: map f L ≤ M эквивалентно L ≤ comap f M.

LaTeX

$$L.map f ≤ M ↔ L ≤ M.comap f$$

Lean4

theorem map_le_iff_le_comap {f : LatticeHom α β} {M : Sublattice β} : L.map f ≤ M ↔ L ≤ M.comap f :=
  image_subset_iff

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

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

Разделы

Аффилиация

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