instAddLeftMono — Mathlib

English

Addition on the left preserves order: if v ≤ w, then u+v ≤ u+w for any fixed vector measure u.

Русский

Прибавление слева сохраняет порядок: если v ≤ w, то для любого фиксированного векторного измерения u выполнено u+v ≤ u+w.

LaTeX

$$∀ u v w, v ≤ w → u+v ≤ u+w$$

Lean4

instance instAddLeftMono : AddLeftMono (VectorMeasure α M) :=
  ⟨fun _ _ _ h i hi => add_le_add_left (h i hi) _⟩

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