le_inv_mul_iff

Mathlib.Algebra.Order.Monoid.Unbundled.Units

URI: https://scilib.ai/kg/mathlib#Units.le_inv_mul_iff

English

For a unit u ∈ M and all a,b ∈ M, a ≤ u⁻¹ b iff u a ≤ b.

Русский

Для единицы u ∈ M и любых a,b ∈ M выполняется a ≤ u⁻¹ b эквивалентно u a ≤ b.

LaTeX

$$$a \le u^{-1} b \iff u a \le b$$$

Lean4

theorem le_inv_mul_iff : a ≤ u⁻¹ * b ↔ u * a ≤ b := by rw [← u.mul_le_mul_iff_left, mul_inv_cancel_left]

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

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

Разделы

Аффилиация

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