Zulip Chat Archive

Stream: maths

Topic: let in statements


view this post on Zulip Patrick Massot (Dec 19 2018 at 19:50):

How does mathlib like using let in order to unclutter a statement, as in:

lemma uniform_continuous₂_iff [uniform_space α] [uniform_space β] [uniform_space γ]
{f : α  β  γ}  :
let π_α : (α × β) × (α × β)  α × α := (λ p, (p.1.1, p.2.1)),
    π_β : (α × β) × (α × β)  β × β := (λ p, (p.1.2, p.2.2)),
    F   : (α × β) × (α × β)  γ × γ := (λ p, (f p.1.1 p.1.2, f p.2.1 p.2.2)) in
uniform_continuous₂ f  map F (comap π_α uniformity  comap π_β uniformity)  uniformity :=
by simp [uniform_continuous,uniformity_prod, tendsto]

view this post on Zulip Patrick Massot (Dec 19 2018 at 19:51):

Of course this is done in a file having set_option eqn_compiler.zeta true

view this post on Zulip Patrick Massot (Dec 19 2018 at 19:53):

Note that the above snippet also use full type ascriptions in lets in order to clarify what are those functions without reading their obscure definition

view this post on Zulip Scott Morrison (Dec 19 2018 at 20:57):

Seems like a good idea.


Last updated: May 11 2021 at 16:22 UTC