## Stream: Is there code for X?

### Topic: More point set topology questions

#### Adam Topaz (Oct 08 2020 at 18:58):

Does mathlib have one and/or both of the following facts?

lemma le_nhds_Lim {X : Type*} [topological_space X] [compact_space X] [nonempty X]
(F : ultrafilter X) : F.1 ≤ nhds (Lim F.1) := sorry

lemma Lim_eq_iff_le_nhds {X : Type*} [topological_space X] [compact_space X] [t2_space X]
[nonempty X] (x : X) (F : ultrafilter X) : Lim F.1 = x ↔ F.1 ≤ nhds x := sorry


#### Adam Topaz (Oct 08 2020 at 19:03):

I have a (currently very messy) proof of the equivalence between compact Hausdorff spaces and the category of algebras for the ultrafilter monad. These would help cleaning it up a bit.

#### Yury G. Kudryashov (Oct 08 2020 at 20:52):

It seems that the answer is "no" but we have docs#compact_iff_ultrafilter_le_nhds and docs#Lim_spec

#### Yury G. Kudryashov (Oct 08 2020 at 20:59):

The second one follows from the first one and docs#Lim_eq.
BTW,

• have a look at the trick I used in docs#Lim_spec to avoid a [nonempty] assumption;
• rename docs#Lim_spec to le_nhds_Lim and docs#lim_spec to tendsto_nhds_lim;
• add Lim_eq_iff (h : ∃ a, Lim f ≤ nhds a) {a} : Lim f = a ↔ F ≤ nhds a and lim_eq_iff (h : ∃ a, tendsto g f (nhds a)) {a} : lim f g = a ↔ tendsto g f a?

#### Adam Topaz (Oct 08 2020 at 21:04):

Right, I've seen docs#compact_iff_ultrafilter_le_nhds docs#Lim_spec and docs#Lim_eq (they're actually used in the linked file above, but I'm still working on cleaning it up). I'm not sure what you mean about the nonempty assumption. It's a little subtle, since one has to use the fact that X is empty if and only if ultrafilter X is empty.

#### Yury G. Kudryashov (Oct 08 2020 at 21:06):

I opened issue #4543.

#### Yury G. Kudryashov (Oct 08 2020 at 21:07):

If you'll try to prove this (do cases on compact_iff_ultrafilter_le_nhds, then use Lim_spec), then the only place where you'll need nonempty is the implicit argument of Lim.

#### Yury G. Kudryashov (Oct 08 2020 at 21:09):

Ah, I see. That's not a problem for the second lemma (you can supply ⟨x⟩ as [nonempty α])

#### Adam Topaz (Oct 08 2020 at 21:10):

And same for the first one, since you have an ultrafilter.

#### Adam Topaz (Oct 08 2020 at 21:11):

The branch above also proves this
https://github.com/leanprover-community/mathlib/blob/ca24ce9856e8d2b4e2d6148f1030cda171c8ba49/src/order/filter/ultrafilter.lean#L267
which gives a nonempty X from nonempty (ultrafilter X).

#### Yury G. Kudryashov (Oct 08 2020 at 21:11):

For the first one you can supply nonempty_of_ne_bot F.1

That's for sets.

I think.

#### Yury G. Kudryashov (Oct 08 2020 at 21:11):

AFAIR, we have an instance {F : ultrafilter α} [ne_bot (F.1)]

#### Yury G. Kudryashov (Oct 08 2020 at 21:11):

docs#filter.nonempty_of_ne_bot

#### Yury G. Kudryashov (Oct 08 2020 at 21:12):

We don't have this instance!

Oops!

#### Yury G. Kudryashov (Oct 08 2020 at 21:13):

Just add it: instance {F : ultrafilter α} : ne_bot F.1 := F.2

#### Yury G. Kudryashov (Oct 08 2020 at 21:14):

I guess our is_ultrafilter API is much better.

#### Yury G. Kudryashov (Oct 08 2020 at 21:14):

If you have time, you may want to migrate mathlib to bundled ultrafilters.

#### Adam Topaz (Oct 08 2020 at 21:15):

I never have time.

#### Adam Topaz (Oct 08 2020 at 21:15):

But I'll try to find some nonexistent time to take care of that issue.

#### Yury G. Kudryashov (Oct 08 2020 at 21:16):

Probably with definition like

structure ultrafilter (α : Type*) :=
(to_filter : filter α)
(ne_bot' : ne_bot to_filter)
(le_of_le' : ∀g, ne_bot g → g ≤ to_filter → to_filter ≤ g)


#### Yury G. Kudryashov (Oct 08 2020 at 21:17):

If you do this, then lemmas assuming is_ultrafilter in order/filter/filter_product can become instances.

#### Adam Topaz (Oct 08 2020 at 21:17):

Why not keep ultrafilter as is, and just restate the lemmas.

#### Yury G. Kudryashov (Oct 08 2020 at 21:40):

I don't think that it makes sense to have both is_ultrafilter and ultrafilter.

#### Yury G. Kudryashov (Oct 08 2020 at 21:41):

If you have an ultrafilter, then most probably (unless it's pure a) it is defined using classical.some, and being an ultrafilter is its main property.

#### Yury G. Kudryashov (Oct 08 2020 at 21:43):

And if you leave only ultrafilter, then using a structure makes it possible to use { to_filter := ..., ne_bot := ..., le_of_le := ... } in a constructor instead of just subtype.mk.

#### Adam Topaz (Oct 08 2020 at 22:08):

@Yury G. Kudryashov
https://github.com/leanprover-community/mathlib/compare/lim_spec_cleanup

I'll wait for github's checks to finish before opening a PR. Is this what you had in mind?

#### Yury G. Kudryashov (Oct 08 2020 at 22:12):

You can use

lemma is_ultrafilter.le_nhds_Lim [compact_space α] (F : ultrafilter α) :
F.1 ≤ nhds (@Lim _ _ F.1.nonempty_of_ne_bot F.1) :=
begin
rcases compact_iff_ultrafilter_le_nhds.mp compact_univ F.1 F.2 (by simp) with ⟨x,_,h⟩,
exact le_nhds_Lim ⟨x,h⟩,
end


#### Adam Topaz (Oct 08 2020 at 22:15):

unknown identifier 'is_compact_univ'
Am I missing an import?

#### Yury G. Kudryashov (Oct 08 2020 at 22:18):

It's compact_univ

#### Yury G. Kudryashov (Oct 08 2020 at 22:19):

Sorry, I made lots of typos. Hopefully, fixed.

#### Adam Topaz (Oct 08 2020 at 22:20):

No worries. Found it now.

#### Adam Topaz (Oct 08 2020 at 22:21):

Pushed the change just now.

#### Adam Topaz (Oct 08 2020 at 22:21):

I'll still wait for the checks to pass, just to make sure the renaming didn't cause any issues I didn't notice.

#### Yury G. Kudryashov (Oct 08 2020 at 22:30):

You can already open a PR. It won't get merged till it passes CI anyway.

#### Adam Topaz (Oct 08 2020 at 22:49):

#4545

Last updated: May 16 2021 at 05:21 UTC