# 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: Dec 20 2023 at 11:08 UTC