inf_eq_div_oneLePart_div — Mathlib

English

For all a,b in a lattice-ordered group with left-mono id, the infimum satisfies a ⊓ b = a / (a / b)⁺ᵐ.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem inf_eq_div_oneLePart_div (a b : α) : a ⊓ b = a / (a / b)⁺ᵐ := by
  simp [oneLePart, div_sup, inf_comm]
    -- Bourbaki A.VI.12 Prop 9 c)

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