comap_mono

Mathlib.Order.Filter.Map

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

English

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

Русский

Фильтр-комап монотонен: если f ≤ g, то comap m f ≤ comap m g.

LaTeX

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

Lean4

@[mono]
theorem comap_mono : Monotone (comap m) :=
  (gc_map_comap m).monotone_u

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

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

Разделы

Аффилиация

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