mabs_sup_div_sup_le_mabs — Mathlib

English

For all a,b,c, the product or comparison yields a bound: |(a ⊔ c)/(b ⊔ c)|_m ≤ |a/b|_m.

Русский

Для любых a,b,c выполняется неравенство: |(a ⊔ c)/(b ⊔ c)|_м ≤ |a/b|_м.

LaTeX

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

Lean4

@[to_additive]
theorem mabs_sup_div_sup_le_mabs (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ := by
  apply le_of_mul_le_of_one_le_left _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]

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