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.

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.

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'