map_mono

Mathlib.Order.Sublattice

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

English

The operation of taking the image of a Sublattice under a lattice homomorphism is monotone: if L ≤ M then L.map f ≤ M.map f.

Русский

Операция образа подрешётки через гомоморфизм решёток монотонна: если L ≤ M, то L.map f ≤ M.map f.

LaTeX

$$L \\le M \\Rightarrow L.map f \\le M.map f$$

Lean4

theorem map_mono : Monotone (map f) := fun _ _ ↦ image_mono

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

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

Разделы

Аффилиация

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