oneLePart_inf_leOnePart_eq_one — Mathlib

English

In any lattice-ordered group, the positive part a⁺ᵐ and the negative part a⁻ᵐ meet at the identity: a⁺ᵐ ⊓ a⁻ᵐ = 1.

Русский

В любой упорядоченной по частям группе положительная часть элемента a и отрицательная часть a взаимно сведены к единице: a⁺ᵐ ⊓ a⁻ᵐ = 1.

LaTeX

$$$a^{+m} \wedge a^{-m} = 1$$$

Lean4

@[to_additive]
theorem oneLePart_inf_leOnePart_eq_one (a : α) : a⁺ᵐ ⊓ a⁻ᵐ = 1 := by
  rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv, oneLePart_div_leOnePart,
    leOnePart_eq_inv_inf_one, inv_inv]

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