ext_nonempty — Mathlib

English

If μ₁ and μ₂ agree on all nonempty sets, then μ₁ = μ₂.

Русский

Если μ₁ и μ₂ совпадают на всех непустых множествах, то μ₁ = μ₂.

LaTeX

$$$\\\\forall s \\\\ (s\\\\neq \\\\emptyset) \\\\Rightarrow μ_1(s)=μ_2(s) \\\\Rightarrow μ_1=μ_2$$$

Lean4

/-- A version of `MeasureTheory.OuterMeasure.ext` that assumes `μ₁ s = μ₂ s` on all *nonempty*
sets `s`, and gets `μ₁ ∅ = μ₂ ∅` from `MeasureTheory.OuterMeasure.empty'`. -/
theorem ext_nonempty {μ₁ μ₂ : OuterMeasure α} (h : ∀ s : Set α, s.Nonempty → μ₁ s = μ₂ s) : μ₁ = μ₂ :=
  ext fun s => s.eq_empty_or_nonempty.elim (fun he => by simp [he]) (h s)

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