le_of_add_le_add_left — Mathlib

English

Let μ be a finite measure on α and let ν1, ν2 be measures on α. If μ + ν1 ≤ μ + ν2, then ν1 ≤ ν2.

Русский

Пусть μ — конечная мера на α, а ν1, ν2 — меры на α. Если μ + ν1 ≤ μ + ν2, то ν1 ≤ ν2.

LaTeX

$$$(\mu(\mathrm{univ}) < \infty) \land (\mu + \nu_1 \le \mu + \nu_2) \Rightarrow \nu_1 \le \nu_2$$$

Lean4

/-- `le_of_add_le_add_left` is normally applicable to `OrderedCancelAddCommMonoid`,
but it holds for measures with the additional assumption that μ is finite. -/
theorem le_of_add_le_add_left [IsFiniteMeasure μ] (A2 : μ + ν₁ ≤ μ + ν₂) : ν₁ ≤ ν₂ := fun S =>
  ENNReal.le_of_add_le_add_left (MeasureTheory.measure_ne_top μ S) (A2 S)

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