monovaryOn_inv

Mathlib.Algebra.Order.Monovary

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

English

MonovaryOn f⁻¹ g⁻¹ on s is equivalent to MonovaryOn f g on s.

Русский

MonovaryOn f⁻¹ g⁻¹ на s эквивалентно MonovaryOn f g на s.

LaTeX

$$$$\\operatorname{MonovaryOn}(f^{-1}, g^{-1}, s) \\iff \\operatorname{MonovaryOn}(f, g, s).$$$$

Lean4

@[to_additive]
theorem monovaryOn_inv : MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s := by simp

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

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

Разделы

Аффилиация

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