sup_div_inf_eq_mabs_div — Mathlib

English

The quotient by the infimum and supremum satisfy a relation with the modulus: (a ⊔ b)/(a ⊓ b) = |b/a|_m.

Русский

Деление по максимуму и минимуму связано с модулем: (a ⊔ b)/(a ⊓ b) = |b/a|_м.

LaTeX

$$(a \lor b) / (a \land b) = |b / a|_m$$

Lean4

@[to_additive]
theorem sup_div_inf_eq_mabs_div (a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ :=
  by
  simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]
  rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]
  exact one_le_mabs _

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