Definitions and theorems local to a section?

Stream: new members

[Ching-Tsun Chou]

Can I have definitions and theorems local to a section? By this I mean that they behave like normal definitions and theorems in the section but their names are not available and hence they cannot be referenced outside the section.

[Julian Berman]

Do you want them not referenceable at all or just not referenceable if someone opens the section? The former is private and the latter is protected (and in general I think Lean calls these ... decl modifiers IIRC?) Let's see if they're already in the reference.

[Ching-Tsun Chou]

I just want to be able to make some intermediate definitions and theorems when proving a main result.

[Julian Berman]

I think as far as I've seen protected lemma ... is one usual first option in that case.

[Ching-Tsun Chou]

In #tpil, private is used in an example but not explained. Judging from the example, I guess that's what I want. On the other hand, protected seems to be about namespaces.

[Ruben Van de Velde]

Yeah, private is correct