Long Stone-Cech

Stream: maths

[Patrick Massot]

@Reid Barton https://github.com/leanprover/mathlib/blob/master/src/topology/stone_cech.lean#L253 takes forever to elaborate. Do you care if I change it to:

instance stone_cech.t2_space : t2_space (stone_cech α) :=
begin
  rw t2_iff_ultrafilter,
  rintros g ⟨x⟩ ⟨y⟩ u gx gy,
  apply quotient.sound,
  intros γ tγ h₁ h₂ f hf,
  resetI,
  let ff := stone_cech_extend hf,
  change ff ⟦x⟧ = ff ⟦y⟧,
  have lim : ∀ z : ultrafilter α, g ≤ nhds ⟦z⟧ → tendsto ff g (nhds (ff ⟦z⟧)) :=
  assume z gz,
    calc map ff g ≤ map ff (nhds ⟦z⟧) : map_mono gz
              ... ≤ nhds (ff ⟦z⟧) : (continuous_stone_cech_extend hf).tendsto _,
  exact tendsto_nhds_unique u.1 (lim x gx) (lim y gy)
end

[Patrick Massot]

which I think is also easier to read by the way

[Reid Barton]

If it's faster go for it

[Patrick Massot]

Thanks. I'm asking because this change will be hidden in a large reorganization PR (the second phase of the topology reorganization decided in Amsterdam).

[Reid Barton]

Oh great, are you already working on that?

[Patrick Massot]

Yes. I'm splitting topology.basic and topology.continuity

[Patrick Massot]

And guess what I learned? Non-finishing calls to simp are evil