Stream: new members

Topic: Introducing a new variable

Frédéric Le Roux (Mar 06 2020 at 17:30):

I have a stupid question. What is the Lean equivalent of a sentence like "Let ε =1-d" (assuming d is a variable in the current setting). Typically, in a proof where I have to show the existence of some object, I would like to name the object. Like in the tactic "use 1-d", but introducing a notation.

Kevin Buzzard (Mar 06 2020 at 17:32):

In tactic mode: let ε := 1 - d. But actually I prefer set ε := 1 - d with hε because then hε contains the proof that ε = 1 - d.

Thank you!

Kevin Buzzard (Mar 06 2020 at 17:56):

One thing I noticed at Xena yesterday when writing a proof with an undergraduate was that after set L := factors n with hLn I was forever rewriting hLn, and at the end of it I was beginning to wish that I'd never introduced the notation at all and had just put factors n everywhere instead of L :-)

Last updated: May 14 2021 at 12:18 UTC