Skip to content

Commit

Permalink
doc(Tactic.Measurability): fixed copy paste error from continuity tac…
Browse files Browse the repository at this point in the history
…tic docs (#12683)

Changed "continuity statements" to "measurability statements"
  • Loading branch information
luigi-massacci committed May 5, 2024
1 parent 8c8a6b1 commit 7d9e677
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Measurability.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ attribute [aesop (rule_sets := [Measurable]) unfold norm] Function.comp
attribute [aesop (rule_sets := [Measurable]) norm] npowRec

/--
The `measurability` attribute used to tag continuity statements for the `measurability` tactic. -/
The `measurability` attribute used to tag measurability statements for the `measurability` tactic.-/
macro "measurability" : attr =>
`(attr|aesop safe apply (rule_sets := [$(Lean.mkIdent `Measurable):ident]))

Expand Down

0 comments on commit 7d9e677

Please sign in to comment.