mabs_inf_div_inf_le_mabs — Mathlib

English

For all a,b,c, |(a ⊓ c)/(b ⊓ c)|_m ≤ |a/b|_m.

Русский

Для любых a,b,c: |(a ⊓ c)/(b ⊓ c)|_м ≤ |a/b|_м.

LaTeX

$$|(a \land c)/(b \land c)|_m ≤ |a / b|_m$$

Lean4

@[to_additive]
theorem mabs_inf_div_inf_le_mabs (a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ := by
  apply le_of_mul_le_of_one_le_right _ (one_le_mabs _);
  rw [mabs_div_sup_mul_mabs_div_inf]
    -- Commutative case, Zaanen, 3rd lecture
    -- For the non-commutative case, see Birkhoff Theorem 19 (27)

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