inf_sq_eq_mul_div_mabs_div — Mathlib

English

A product of two modulus-divisions equals the modulus of a quotient: |(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 ⊔ c)/(b ⊔ c)|_m \cdot |(a ⊓ c)/(b ⊓ c)|_m = |a / b|_m$$

Lean4

@[to_additive two_nsmul_inf_eq_add_sub_abs_sub]
theorem inf_sq_eq_mul_div_mabs_div (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ := by
  rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv, mul_assoc,
    mul_inv_cancel_comm_assoc, ← pow_two]
    -- See, e.g. Zaanen, Lectures on Riesz Spaces
    -- 3rd lecture

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