monovary_id_iff

Mathlib.Order.Monotone.Monovary

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

English

Monovary f id s is equivalent to MonotoneOn f s.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem monovary_id_iff : Monovary f id ↔ Monotone f :=
  monotone_iff_forall_lt.symm

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

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

Разделы

Аффилиация

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