instCanonicallyOrderedAddOfAddLeftMono

English

If α is a canonically ordered additively commutative monoid, then the finsupp type ι →₀ α inherits CanonicallyOrderedAdd, i.e., 0 ≤ f and f ≤ g implies f + h ≤ g + h, etc.

Русский

Если α — канонически упорядоченный аддитивный коммутативный моноид, тогда FinSupp ι α наследует CanonicallyOrderedAdd: 0 ≤ f и f ≤ g приводят к f + h ≤ g + h и т. п.

LaTeX

$$$ CanonicallyOrderedAdd(ι \\to_0 α)$$$

Lean4

instance [AddLeftMono α] : CanonicallyOrderedAdd (ι →₀ α)
    where
  exists_add_of_le := fun {f g} h => ⟨g - f, ext fun x => (add_tsub_cancel_of_le <| h x).symm⟩
  le_add_self _ _ _ := le_add_self
  le_self_add := fun _f _g _x => le_self_add

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