m_Birkhoff_inequalities — Mathlib

English

A combined inequality bounds the sum of the two mabs quotients by the mabs of a/b: |(a ⊔ c)/(b ⊔ c)|_m ⊔ |(a ⊓ c)/(b ⊓ c)|_m ≤ |a/b|_m.

Русский

Композитное неравенство ограничивает максимум двух модулей частного над модулем частного: |(a ⊔ c)/(b ⊔ c)|_м ∨ |(a ⊓ c)/(b ⊓ c)|_м ≤ |a/b|_м.

LaTeX

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

Lean4

@[to_additive Birkhoff_inequalities]
theorem m_Birkhoff_inequalities (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ⊔ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ :=
  sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c)

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