monotone_map_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.monotone_map_iff

English

Monotone map equivalence: Monotone (WithTop.map f) iff Monotone f.

Русский

Эквивалентность монотонности отображения: Monotone(WithTop.map f) ⇔ Monotone f.

LaTeX

$$$$ \\text{Monotone}(\\mathrm{WithTop.map} f) \\iff \\text{Monotone}(f). $$$$

Lean4

@[simp]
theorem monotone_map_iff {f : α → β} : Monotone (WithTop.map f) ↔ Monotone f :=
  monotone_iff.trans <| by simp [Monotone]

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

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

Разделы

Аффилиация

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