monovaryOn_id_iff

Mathlib.Order.Monotone.Monovary

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

English

MonovaryOn f id s is equivalent to MonotoneOn f s.

Русский

MonovaryOn f id s эквивалентно MonotoneOn f s.

LaTeX

$$$\operatorname{MonovaryOn}(f,\mathrm{id},s) \iff \operatorname{MonotoneOn}(f,s)$$$

Lean4

@[simp]
theorem monovaryOn_id_iff : MonovaryOn f id s ↔ MonotoneOn f s :=
  monotoneOn_iff_forall_lt.symm

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

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

Разделы

Аффилиация

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