## Stream: maths

### Topic: let in statements

#### 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]


#### Patrick Massot (Dec 19 2018 at 19:51):

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

#### 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

#### Scott Morrison (Dec 19 2018 at 20:57):

Seems like a good idea.

Last updated: May 11 2021 at 16:22 UTC