local definition to a section ?

Stream: new members

[Nicolas Rolland]

Can I make some definitions local to a section, so that reusing the names in another does not clash ?

import Mathlib.CategoryTheory.Adjunction.Basic

section MySection

lemma _aname : True := sorry

end MySection

section OtherSection

-- lemma _aname : True := sorry --  '_aname' has already been declared

end OtherSection

The intended usage of those throwaway names is to make some other definitions in the same section more readable

[Kyle Miller]

It's not section local, but you can use private lemma to make it not appear outside the module.

[Kyle Miller]

Mathlib doesn't use _ prefixes for local things by the way. Sometimes you see an aux suffix, or the lemma just follows the usual naming convention. Or often it turns out there's not really a need for things to be private, unless it's truly a single-use highly technical lemma.

[Edward van de Meent]

i think ' as a postfix also gets used for this...