dual

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#AntivaryOn.dual

English

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

Русский

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

LaTeX

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

Lean4

theorem dual : AntivaryOn f g s → AntivaryOn (toDual ∘ f) (toDual ∘ g) s :=
  swap₂

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

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

Разделы

Аффилиация

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