monotoneOn_univ

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#monotoneOn_univ

English

MonotoneOn on the universal set is equivalent to Monotone.

Русский

Монотонность на всём множестве эквивалентна монотонности самой функции.

LaTeX

$$$\operatorname{MonotoneOn}(f,\mathrm{Set.univ}) \leftrightarrow \operatorname{Monotone}(f)$$$

Lean4

@[simp]
theorem monotoneOn_univ : MonotoneOn f Set.univ ↔ Monotone f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.monotoneOn _⟩

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

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

Разделы

Аффилиация

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