ext_of_singleton — Mathlib

English

On a countable space, two measures are equal if they take the same value on every singleton.

Русский

На счётном пространстве две меры равны, если они одинаковы на каждом одномерном множестве {a}.

LaTeX

$$$ [Countable \\alpha] \\{ \\mu \\ {a} = \\nu {a} \\ for \\ all \\ a \\} \\Rightarrow μ = ν $$$

Lean4

/-- Two measures on a countable space are equal if they agree on singletons. -/
theorem ext_of_singleton [Countable α] {μ ν : Measure α} (h : ∀ a, μ { a } = ν { a }) : μ = ν :=
  ext_of_sUnion_eq_univ (countable_range singleton) (by aesop) (by simp_all)

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