antivary_inv_left₀

Mathlib.Algebra.Order.Monovary

URI: https://scilib.ai/kg/mathlib#antivary_inv_left₀

English

If StrongLT 0 on f, Antivary f^{-1} g is equivalent to Monovary f g.

Русский

Пусть StrongLT 0 на f, тогда Antivary f^{-1} g эквивалентно Monovary f g.

LaTeX

$$$\\text{StrongLT }0 f \\Rightarrow \\bigl(\\text{Antivary}(f^{-1},g) \\iff \\text{Monovary}(f,g)\\bigr)$$$

Lean4

@[simp]
theorem antivary_inv_left₀ (hf : StrongLT 0 f) : Antivary f⁻¹ g ↔ Monovary f g :=
  forall₃_congr fun _i _j _ ↦ inv_le_inv₀ (hf _) (hf _)

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

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

Разделы

Аффилиация

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