sup_sq_eq_mul_mul_mabs_div — Mathlib

English

The square of the supremum equals the product of the two operands times the modulus of the quotient: (a ⊔ b)^2 = a b |b/a|_m.

Русский

Квадрат верхнего предела равен произведению элементов, умноженному на модуль частного: (a ⊔ b)^2 = a b |b/a|_м.

LaTeX

$$(a \lor b)^2 = a \cdot b \cdot |b / a|_m$$

Lean4

@[to_additive two_nsmul_sup_eq_add_add_abs_sub]
theorem sup_sq_eq_mul_mul_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, ← mul_assoc, mul_comm, mul_assoc, ← pow_two,
    inv_mul_cancel_left]

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