proper names for parts of a lean proof (beginner)

Stream: new members

[rzeta0]

Attached is a diagram I created to help make my question clearer.

1. Is the first line a theorem, or is it just a proof header? (the first line sets out the name, variable types, hypothesis, and the overlall proof objective/goal)
2. Is the whole block, first line to concluding line, called a proof, or is the proof only the part after the header / theorem statement?

After 2 weeks of reading, following online courses, I haven't found anything that clearly states what these are.

Imho the following sounds right:

• the first line is the theorem because it states the conclusion (objective/goal) and the context (variable types, antecedent hypotheses)
• the proof is the whole block including the statement of the theorem

header_theorem.png

[Kyle Miller]

I would say the entire thing is the theorem.

The example/theorem/lemma doesn't have a name. You could call it the "example keyword", "theorem keyword" or "lemma keyword" for the "example/theorem/lemma command".

The identifier that follows theorem or lemma is the "theorem/lemma name". The example command does not have a theorem name.

Everything until the : is a "hypothesis"/"variable"/"parameter"/"binder" (all pretty much interchangeable, but it might feel more comfortable using one of these over the other depending on what the variable is for). There is no type/hypothesis distinction like you have in your diagram. There are a number of "binder types" like {...} vs (...) vs [...], but these have no impact on the theorem statement itself, only on how the theorem is instantiated in later proofs.

The "theorem statement" comprises all the variables and the type after the :, up to the :=.

What's after the := is called the "theorem body" or the "proof of the theorem".

[Kyle Miller]

I'm not sure if there's an official terminology for any of this. I'm just going by how I hear people talk about it.

[rzeta0]

Is the use of different binder types  {...} vs (...) vs [...] considered advanced usage, or is it something beginners will need for basic proofs too?

I'm try to work out what teach of those binder types does ...

• {...} is to variables
• (...) is for statements with some relation eg =, <, >= ... (hypotheses)
• [...] ?? what are these used for?

When you say the entire thing is a theorem, is that a common consensus view? I ask because to me the whole thing is a proof (a proof can't exclude what it is trying to prove), but a theorem is often stated in books/papers without a proof.

[Kyle Miller]

Certainly it's the case that the whole thing is the theorem command. I don't know what you'd gain by splitting it further.

[Ruben Van de Velde]

[] are for type class arguments; () are for explicit argument; {} are for implicit arguments (which can generally be found by looking at later explicit arguments)

[Ruben Van de Velde]

I guess you could split a "theorem" into a "theorem statement" and a "proof"

[Kyle Miller]

[...] which can generally be found by looking at later explicit arguments

or after :

[Kyle Miller]

Ruben Van de Velde said:

I guess you could split a "theorem" into a "theorem statement" and a "proof"

I already made that split earlier