antivaryOn_toDual_left

Mathlib.Order.Monotone.Monovary

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

English

If AntivaryOn (toDual ∘ f) g s then MonovaryOn f g s.

Русский

Если AntivaryOn (toDual ∘ f) g s, то MonovaryOn f g s.

LaTeX

$$$\operatorname{AntivaryOn}(\mathrm{toDual} \circ f, g, s) \Rightarrow \operatorname{MonovaryOn}(f, g, s)$$$

Lean4

@[simp]
theorem antivaryOn_toDual_left : AntivaryOn (toDual ∘ f) g s ↔ MonovaryOn f g s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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