sup_eq_mul_oneLePart_div — Mathlib

English

For all a,b in a lattice-ordered group, the join a ⊔ b equals b multiplied by the positive part of a/b: a ⊔ b = b · (a / b)⁺ᵐ.

Русский

Для любых a,b в упорядоченной по группе группе объединение a ⊔ b равно произведению b на положительную часть от (a/b): a ⊔ b = b · (a / b)⁺ᵐ.

LaTeX

$$$a \vee b = b \cdot (a / b)^{+m}$$$

Lean4

@[to_additive]
theorem sup_eq_mul_oneLePart_div (a b : α) : a ⊔ b = b * (a / b)⁺ᵐ := by
  simp [oneLePart, mul_sup]
    -- Bourbaki A.VI.12 (with a and b swapped)

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