antivaryOn_toDual_right

Mathlib.Order.Monotone.Monovary

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem antivaryOn_toDual_right : AntivaryOn f (toDual ∘ g) s ↔ MonovaryOn f g s :=
  forall₂_swap

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

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

Разделы

Аффилиация

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