monovaryOn_iff_monovary

Mathlib.Order.Monotone.Monovary

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

English

MonovaryOn f g s is equivalent to Monovary (λ i : s, f i) (λ i : s, g i).

Русский

MonovaryOn f g s эквивалентно Monovary (λ i : s, f i) (λ i : s, g i).

LaTeX

$$$MonovaryOn(f,g,s) \iff Monovary(\lambda i:s. f i) (\lambda i:s. g i)$$$

Lean4

theorem monovaryOn_iff_monovary : MonovaryOn f g s ↔ Monovary (fun i : s ↦ f i) fun i ↦ g i := by
  simp [Monovary, MonovaryOn]

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

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

Разделы

Аффилиация

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