Skip to content

Commit 4f11cc9

Browse files
committed
Update Real.lean
1 parent ff9a55a commit 4f11cc9

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/MeasureTheory/Integral/RieszMarkovKakutani

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,7 @@ then they are equal. -/
399399
theorem _root_.MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported
400400
[μ.Regular] [ν.Regular] (hμν : ∀ f : C_c(X, ℝ), ∫ x, f x ∂μ = ∫ x, f x ∂ν) :
401401
μ = ν := by
402-
apply Measure.OuterRegular.eq_of_eq_on_isOpen
402+
apply Measure.OuterRegular.ext_isOpen
403403
apply Measure.InnerRegularWRT.eq_on_outer_of_eq_on_inner Measure.Regular.innerRegular
404404
Measure.Regular.innerRegular
405405
intro K hK

0 commit comments

Comments
 (0)