Zulip Chat Archive

Stream: maths

Topic: exponentials


view this post on Zulip Kenny Lau (Apr 27 2018 at 14:06):

@Chris Hughes what happened to your PR's about exp?

view this post on Zulip Chris Hughes (Apr 27 2018 at 15:40):

I made this PR https://github.com/leanprover/mathlib/pull/61 in Feb, which is a necessary part of exp, and it hasn't been closed or accepted essentially because I didn't use filters, I used cau_seq as defined in data.real.cau_seq. I might have to rewrite it using filters over the summer.

view this post on Zulip Kenny Lau (Apr 27 2018 at 15:41):

I'm also trying to learn how filters define limit :D

view this post on Zulip Kenny Lau (Apr 27 2018 at 15:41):

theorem const (x : X) (y : Y) : tendsto (λ _ : X, y) (nhds x) (nhds y) :=
λ B HB FX HF1, HF1 _ set.univ, rfl $ univ_mem_sets' $
λ x, show y  B, from mem_of_nhds HB

This was an exercise I set to myself (I know it's in mathlib already)


Last updated: May 12 2021 at 08:14 UTC