inv_mul_le_one

Mathlib.Algebra.Order.Monoid.Unbundled.Units

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

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 inv_mul_le_one : u⁻¹ * a ≤ 1 ↔ a ≤ u := by rw [u.inv_mul_le_iff, mul_one]

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

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

Разделы

Аффилиация

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