add_right_inj — Mathlib

English

For σ-finite μ, μ + ν1 = μ + ν2 implies ν1 = ν2, and conversely.

Русский

Для сигма-конечной μ, μ + ν1 = μ + ν2 тогда и только тогда, когда ν1 = ν2.

LaTeX

$$$[SigmaFinite μ] : μ + ν_1 = μ + ν_2 \iff ν_1 = ν_2$$$

Lean4

@[simp]
theorem add_right_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] : μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  rw [ext_iff_of_iUnion_eq_univ (iUnion_spanningSets μ)]
  intro i
  ext s hs
  rw [← ENNReal.add_right_inj (measure_mono s.inter_subset_right |>.trans_lt <| measure_spanningSets_lt_top μ i).ne]
  simp only [ext_iff', coe_add, Pi.add_apply] at h
  simp [hs, h]

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