map_mono

Mathlib.Order.Filter.Map

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

English

The map operation is monotone: if f ≤ g then map m f ≤ map m g.

Русский

Операция отображения монотонна: если f ≤ g, то map m f ≤ map m g.

LaTeX

$$$\\text{Monotone}(\\mathrm{map}\\ m)$$$

Lean4

@[mono]
theorem map_mono : Monotone (map m) :=
  (gc_map_comap m).monotone_l

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

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

Разделы

Аффилиация

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