add_left_inj

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.add_left_inj

← MathLib Explorer

English

If ν1 + μ = ν2 + μ and μ is σ-finite, then ν1 = ν2.

Русский

Если ν1 + μ = ν2 + μ и μ сигма-конечна, то ν1 = ν2.

LaTeX

$$@[simp] theorem add_left_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] : ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂$$

Lean4

@[simp]
theorem add_left_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] : ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂ := by
  rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru