let in statements

Stream: maths

[Patrick Massot]

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]

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

[Patrick Massot]

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]

Seems like a good idea.