mul_right

Mathlib.Algebra.Order.Monovary

URI: https://scilib.ai/kg/mathlib#MonovaryOn.mul_right

← MathLib Explorer

English

Monovary f⁻¹ g⁻¹ is equivalent to Monovary f g.

Русский

Monovary f⁻¹ g⁻¹ эквивалентна Monovary f g.

LaTeX

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

Lean4

@[to_additive]
theorem mul_right (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : MonovaryOn f (g₁ * g₂) s := fun _i hi _j hj hij ↦
  (lt_or_lt_of_mul_lt_mul hij).elim (h₁ hi hj) <| h₂ hi hj

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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