# Extensionality of finite measures #

The main Result is `ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable`: Let `A` be a StarSubalgebra of `C(E, 𝕜)` that separates points and whose elements are bounded. If the integrals of all elements of `A` with respect to two finite measures `P, P'`coincide, then the measures coincide. In other words: If a Subalgebra separates points, it separates finite measures.

source
theorem MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [MeasurableSpace E] [PseudoEMetricSpace E] [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] {P P' : Measure E} [IsFiniteMeasure P] [IsFiniteMeasure P'] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') :
P = P'

If the integrals of all elements of a subalgebra `A` of continuous and bounded functions with respect to two finite measures `P, P'` coincide, then the measures coincide. In other words: If a subalgebra separates points, it separates finite measures.

source
theorem MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [MeasurableSpace E] [TopologicalSpace E] [PolishSpace E] [BorelSpace E] {P P' : Measure E} [IsFiniteMeasure P] [IsFiniteMeasure P'] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') :
P = P'