Zulip Chat Archive

Stream: general

Topic: on incomprehensibility

Reid Barton (Oct 20 2018 at 02:01):

I managed to turn a screen-long argument (Theorem 4.3 here) which I don't really understand into 4 lines of lean which I also don't really understand--the last four lines below. (What I'm formalizing is not exactly the same thing as that page is talking about, but I think it's closely related.)

import analysis.topology.continuity

open filter

universe u

structure convergence (α : Type u) : Type (u+1) :=
(r : Π (n : Type u) (ω : ultrafilter n), (n  α)  α  Prop)
(H :  (n : Type u) (f : n  α) (ω : ultrafilter n) (a : α),
     r α (ω.map f) id a  r n ω f a)
(I :  (a : α), r α (pure a) id a)
(J :  (n m : Type u) (ω : ultrafilter n) (ξ : n  ultrafilter m)
       (f : n  α) (g : m  α) (a : α),
     ( (i : n), r m (ξ i) g (f i))  r n ω f a  r m (ω.bind ξ) g a)

variables {α : Type u}

def convergence_of_topology (t : topological_space α) : convergence α :=
{ r := λ n ω f x,  u  (nhds x).sets, {i | f i  u}  ω.val.sets,
  H := assume n f ω a h, h,
  I := assume a, pure_le_nhds a,
  J := assume n m ω ξ f g a h₁, h₂ u hu,
    let v, vu, vo, av := mem_nhds_sets_iff.mp hu in
    ω.val.sets_of_superset (h₂ v (mem_nhds_sets vo av))
      (λ i hi, h₁ _ _ (mem_nhds_sets_iff.mpr v, vu, vo, hi)) }

Reid Barton (Oct 20 2018 at 02:03):

I don't really have any point here except to say that sometimes the original math proofs aren't really that much more comprehensible than mathlib-style golfed proofs.

Reid Barton (Oct 20 2018 at 02:17):

Also, I learned "why" this statement J is true (it's somehow exactly because the neighborhood filter of a point a is generated by sets v which are also neighborhoods of all their elements, namely the open sets), but I still don't really understand what the statement says

Mario Carneiro (Oct 20 2018 at 03:20):

it might help if you gave things more than one letter names :)

Last updated: Aug 03 2023 at 10:10 UTC