Zulip Chat Archive

Stream: new members

Topic: Substituting variable in lamda abstraction in goal


view this post on Zulip Saif Ghobash (Dec 30 2020 at 16:04):

I have the following hypothesis and goal,

1 goal
ω: 
hωpos: ω > 0
N: 
H1_h: 1 / ω < N
n: 
hnN: n > N
 abs ((λ (n : ), 1 / n) n) < ω

I would like to substitute the n in the lambda abstraction with the n in my hypothesis

view this post on Zulip Adam Topaz (Dec 30 2020 at 16:05):

dsimp only

view this post on Zulip Saif Ghobash (Dec 30 2020 at 16:05):

Thank you!

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 16:26):

I am always embarrassed by how difficult it is to prove that 1/n tends to 0 from first principles in Lean :-)

view this post on Zulip Johan Commelin (Dec 30 2020 at 16:30):

@Saif Ghobash Are writing some form of lecture notes accompanied by Lean proofs?

view this post on Zulip Johan Commelin (Dec 30 2020 at 16:30):

If so, you might be interested in lean_formatter and possibly also the framework used by "Mathematics in Lean".

view this post on Zulip Saif Ghobash (Dec 30 2020 at 17:13):

@Johan Commelin I am an undergraduate rewriting my professors lecture notes in lean as a way to learn lean and study for my real analysis finals. :smile:

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:15):

That's a great way to do it. You should make a little repo where you put up stuff. I was working on some undergraduate problem sheets for analysis with some Imperial first year undergraduates -- I wasn't teaching the course, we were just goofing around. https://github.com/ImperialCollegeLondon/M40002

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:17):

You should just make a github project for your class, with mathlib as a dependency, and then within src set up a nice directory structure (lectures, problem sheets, exam questions, whatever) and start dumping Lean files in the directories and showing other kids in your class. Explain in your README how to install your project (just copy what I wrote mutatis mutandis) and see if other people contribute.

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:18):

@Saif Ghobash

view this post on Zulip Saif Ghobash (Dec 30 2020 at 17:19):

@Kevin Buzzard I might just do that, it was actually a lot of your posts on the Xena website that made me want to get into Lean in the first place :smiley: , the website has been a fantastic resource

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:20):

let me know what you want me to write about. I've been neglecting it recently.

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:21):

I've got a deadline of NYE to submit a paper but can think about a new year post

view this post on Zulip Bryan Gin-ge Chen (Dec 30 2020 at 17:22):

Since you've been working on some mathlib PRs recently, maybe you could write about one of those?

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 17:23):

oh that's an interesting idea!


Last updated: May 10 2021 at 17:39 UTC