instIsOrderedCancelAddMonoid — Mathlib

English

If each α_i is an additive cancellative ordered monoid, then Π₀ i, α_i is an IsOrderedCancelAddMonoid; in particular, a + b ≤ a + c implies b ≤ c.

Русский

Если каждый α_i — аддитивный отменимый упорядоченный моноид, то Π₀ i, α_i тоже упорядоченный отменимый монойд; в частности, a + b ≤ a + c => b ≤ c.

LaTeX

$$$$ a + b \\le a + c \\Rightarrow b \\le c. $$$$

Lean4

instance (α : ι → Type*) [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsOrderedCancelAddMonoid (α i)] :
    IsOrderedCancelAddMonoid (Π₀ i, α i) :=
  { le_of_add_le_add_left := fun _ _ _ H i ↦ le_of_add_le_add_left (H i) }

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