addLeftReflectLE — Mathlib

English

If h is left-cancellative with respect to addition, then l.e. on finsupp is preserved under addition on the left.

Русский

Если сложение слева сохраняет неравенство, то неравенство сохраняется при добавлении слева на ι →₀ α.

LaTeX

$$le_of_add_le_add_left (∀ s, ... )$$

Lean4

instance addLeftReflectLE [AddCommMonoid α] [PartialOrder α] [AddLeftReflectLE α] : AddLeftReflectLE (ι →₀ α) :=
  ⟨fun _f _g _h H x => le_of_add_le_add_left <| H x⟩

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