monotoneOn_singleton

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.monotoneOn_singleton

English

Monotonicity on a singleton set: if the domain is {a}, then f is monotone on {a}.

Русский

Монотонность на множестве-одиночке: если область определения — {a}, то f монотонна на {a}.

LaTeX

$$$ \text{MonotoneOn}(f, \{ a \})$$$

Lean4

@[simp]
theorem monotoneOn_singleton : MonotoneOn f { a } :=
  subsingleton_singleton.monotoneOn f

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

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

Разделы

Аффилиация

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