ext_iff_singleton — Mathlib

English

For a countable α, μ = ν if and only if μ({a}) = ν({a}) for all a.

Русский

Для счётного α, μ = ν тогда и только тогда, когда μ({a}) = ν({a}) для каждого a.

LaTeX

$$$ [Countable \\alpha] \\ μ = ν \\iff ∀ a, μ {a} = ν {a} $$$

Lean4

/-- Two measures on a countable space are equal if and only if they agree on singletons. -/
theorem ext_iff_singleton [Countable α] {μ ν : Measure α} : μ = ν ↔ ∀ a, μ { a } = ν { a } :=
  ⟨fun h _ ↦ h ▸ rfl, ext_of_singleton⟩

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