Zulip Chat Archive

Stream: maths

Topic: Long Stone-Cech


Patrick Massot (Jan 22 2019 at 11:51):

@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 γ  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 (Jan 22 2019 at 11:51):

which I think is also easier to read by the way

Reid Barton (Jan 22 2019 at 11:56):

If it's faster go for it

Patrick Massot (Jan 22 2019 at 12:00):

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 (Jan 22 2019 at 12:00):

Oh great, are you already working on that?

Patrick Massot (Jan 22 2019 at 12:01):

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

Patrick Massot (Jan 22 2019 at 12:20):

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


Last updated: Dec 20 2023 at 11:08 UTC