Topology of `ENat`

Stream: mathlib4

[Etienne Marion]

Hello!
I noticed that there is no topology instantiated for ENat. I need the order topology for a project (neighberhoods of infinity are sets which contain all big enough integers), which makes it a compact space (it's the one-point compactification of Nat). However one could prefer to use the discrete topology instead. My questions are:

1. Is there a drawback defining one of the instance compared to defining none and always use the topology locally?
2. If not, could I define the instance with the order topology, or should I use the topology locally?

[Peter Nelson]

I did this for my matroid repo - see here. I never got round to PRing it and it’s a few months stale, but I would love to see someone pick it up!

[Peter Nelson]

(It was produced by cribbing from the equivalent file for ENNReal)

[Peter Nelson]

To answer your question, I think the discrete topology is probably not the right choice. The order topology allows arbitrary sums of terms in ENat to behave correctly with tsum.

[Etienne Marion]

Thanks for your answer!

Peter Nelson said:

I did this for my matroid repo - see here.

I only need the very basics, so your file has everything (and much more). However I don't think I will be able to deal with such a huge PR I didn't right. Would it be ok for you if I only PR the very basic results? (for now at least)

[Patrick Massot]

I am pretty sure @Dagur Asgeirsson must have done that.

[Etienne Marion]

In fact I discovered docs#OnePoint, which has everything I want except T2 instance, which I'm adding now. It makes more sense in what I'm doing, although of course it's the same topology for ENat.

[Dagur Asgeirsson]

T2 is certainly already there, the file Mathlib.Topology.Category.LightProfinite.Sequence defines the light profinite set $\mathbb{N} \cup \{\infty\}$ as the one point compactification of $\mathbb{N}$. docs#LightProfinite.continuous_iff_convergent proves that a function out of it is continuous iff the corresponding sequence converges to the value at $\infty$.

[Etienne Marion]

This is also in Mathlib.Topology.Compactification.OnePoint as a matter of fact. Anyway I meant the T2 instance in the general case of docs#OnePoint.

[Dagur Asgeirsson]

It would make sense to move the MetrizableSpace instance to a different file if you are going to use OnePoint \N without mentioning LightProfinite

[Etienne Marion]

(deleted)

[Rida Hamadani]

Peter Nelson said:

I did this for my matroid repo - see here. I never got round to PRing it and it’s a few months stale, but I would love to see someone pick it up!

@Joachim Breitner The proof of #15344 will become:

lemma iSup_add (ι : Type*) [Nonempty ι] (f : ι → ℕ∞) (n : ℕ∞) :
    (⨆ x, f x) + n = (⨆ x, f x + n) :=
  Monotone.map_iSup_of_continuousAt' (continuousAt_id.add continuousAt_const) <|
    monotone_id.add monotone_const

After porting this, so I suggest not going the route in #15344.

[Rida Hamadani]

One option is to make #15344 depend on #15380, which is a partial port of Peter's code, just enough to make the proof above work.

[Joachim Breitner]

Thanks, that's great!

[Joachim Breitner]

Indeed, with  #15380 I don’t even strictly need iSup_add . Thanks! (Is it expected that the continuity tactic won’t solve the first goal?)

[Ruben Van de Velde]

Does fun_prop work?

[Joachim Breitner]

Indeed, fun_prop can solve

⊢ ContinuousAt (fun x ↦ x + n) (⨆ x, ↑(↑x).length)

It does not solve

⊢ Monotone fun x ↦ x + n

though, because

`Monotone fun x ↦ x + n` is not a `fun_prop` goal! Maybe you forgot marking `Monotone` with `@[fun_prop]`.

Is there a reason why continuity is monotonicity isn’t a fun_prop goal?

[Ruben Van de Velde]

Nobody's implemented it yet

[Joachim Breitner]

Good reason, as usual :-)