Skip to content

Commit

Permalink
chore: fix a typo in a docstring (#5430)
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Jun 24, 2023
1 parent ceb42c5 commit 637e048
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/MeasureTheory/Measure/Regular.lean
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ class Regular (μ : Measure α) extends IsFiniteMeasureOnCompacts μ, OuterRegul
/-- A measure `μ` is weakly regular if
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using closed sets:
`μ(U) = sup {μ(F) | F ⊆ U compact}` for `U` open. -/
`μ(U) = sup {μ(F) | F ⊆ U closed}` for `U` open. -/
class WeaklyRegular (μ : Measure α) extends OuterRegular μ : Prop where
protected innerRegular : InnerRegular μ IsClosed IsOpen
#align measure_theory.measure.weakly_regular MeasureTheory.Measure.WeaklyRegular
Expand Down

0 comments on commit 637e048

Please sign in to comment.