map_mono

Mathlib.Order.BooleanSubalgebra

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

English

The map operation is monotone: if L ≤ M, then L.map f ≤ M.map f.

Русский

Отображение подалгебры через 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