Closedness is a local property

Stream: Is there code for X?

[Yaël Dillies]

Do we have somewhere that a set is closed if its intersection with every compact set is closed? I need this for ℝⁿ.

[Jireh Loreaux]

I think you'll need to assume your space is locally compact for this to be true (maybe that's obvious to you).

[Filippo A. E. Nuccio]

For $\mathbb{R}^n$ you could use (the complement of) docs#metric.is_open_iff using that compacts are closed and bounded.

[Sophie Morel]

Jireh Loreaux said:

I think you'll need to assume your space is locally compact for this to be true (maybe that's obvious to you).

"Compactly generated" is enough (in fact it's equivalent to the statement that Yaël wanted); Hausdorff locally compact spaces and metric spaces are compactly generated. That kind of space plays a big role in condensed maths, so maybe they're already formalized (Filippo would know better), but I don't know whether they are in mathlib already (I couldn't find them).

[Yaël Dillies]

docs#t2_space, docs#locally_compact_space, docs#metric_space

[Johan Commelin]

For LTE we didn't formalize anything about qs condensed sets, and not really anything about cgHaus spaces. The only thing that comes close is what we called "compHaus-ly filtered pseudo-normed groups": abelian groups $M$ with an $ℝ≥0$-indexed system of subsets that are CH-spaces that satisfy:

• $M_{c₁} + M_{c₂} ⊆ M_{c₁ + c₂}$ and $-M_c = M_c$ and $0 ∈ M_c$
• if $c₁ ≤ c₂$, then $M_{c₁}$ is a closed subset of $M_{c₂}$

and most of the time: $M = ⋃ M_c$.

[Sophie Morel]

@Yaël Dillies I was actually asking about cg (= compactly generated) spaces in mathlib, as I trusted you guys to have already implemented metric spaces etc. :smile:
A topological space X is called cg if, for every subset Y of X, we have that Y is closed if and only if the intersection of Y with every compact subspace K of X is closed in K. (Here "compact" does not include T2, just like in mathlib.) If X is Hausdorff, the last condition is equivalent to Y \cap K being closed in X.
So your question could be reinterpreted as "is R^n a cg space ?" and my answer was "yes because metric spaces are known to be cg, but that might not be in mathlib yet". Anyway I had stuff to do, so I wrote a proof that metric spaces are cg in order to procrastinate. :oops:

import topology.metric_space.basic
import topology.sequences
import topology.alexandroff
import tactic

variables {α : Type*} [metric_space α]


def sequence_and_point_to_map (u : ℕ → α) (l : α) : alexandroff ℕ → α :=
option.elim l u

lemma sequence_and_limit_to_map_is_continuous (u : ℕ → α) (l : α)
(hlim : filter.tendsto u filter.at_top (nhds l)) :
continuous (sequence_and_point_to_map u l) :=
begin
  rw continuous_iff_continuous_at,
  intro x,
  cases x with n,
    {erw alexandroff.continuous_at_infty,
     intros s hs,
     change s ∈ (nhds l) at hs,
     have := hlim hs,
     simp only [filter.mem_map, filter.mem_at_top_sets, ge_iff_le, set.mem_preimage] at this,
     cases this with n hn,
     set t:=set.Icc 0 n with ht,
     existsi t,
     split,
       {exact is_closed_discrete t,},
        split,
          {refine set.finite.is_compact (set.finite_Icc 0 n),
           },
           unfold set.maps_to,
           intros m hm,
           simp only [set.mem_compl_iff, set.mem_Icc, zero_le', true_and, not_le] at hm,
           exact hn m (le_of_lt hm),
     },
     erw alexandroff.continuous_at_coe,
     exact continuous.continuous_at continuous_of_discrete_topology,
end



lemma closed_iff_intersection_with_compacts_is_closed (X : set α) :
(is_closed X) ↔ (∀ (K : set α), (is_compact K) → (is_closed (X ∩ K))) :=
begin
  split,
    {exact λ hX K hK, is_closed.inter hX (is_compact.is_closed hK),},
     intro hX,
     rw ←is_seq_closed_iff_is_closed,
     intros u l hu hlim,
     set f:=sequence_and_point_to_map u l,
     set K:=f '' ⊤,
     have hK : is_compact K :=is_compact.image (alexandroff.compact_space).is_compact_univ
       (sequence_and_limit_to_map_is_continuous u l hlim),
     have : ∀ (n : ℕ), (u n) ∈ (X ∩ K),
       intro n,
       simp only [set.mem_inter_iff, set.mem_image, set.top_eq_univ, set.mem_univ, true_and],
         split,
           {exact hu n,},
            existsi (some n),
            refl,
     exact set.mem_of_mem_inter_left ((is_closed.is_seq_closed (hX K hK)) this hlim),
end

[Johan Commelin]

I agree that cg should be added to mathlib.

[Johan Commelin]

And while we are at it, we should also add compactological spaces to mathlib, because those are exactly the quasi-separated condensed sets.

[Yaël Dillies]

:nerd: :direct_hit:

[Yaël Dillies]

I solved my problem without needing this (see #16976), but I can still try to get cg spaces and compactological spaces into mathlib. Where can I read about the latter? I did not find much online.

[Kevin Buzzard]

If this is going to be a new file, can it go straight to mathlib4? IIRC there seemed to be some agreement that perhaps new file PRs would be acceptable

[Floris van Doorn]

even addition-only PRs to existing files are fine, I think.

[Yaël Dillies]

Oh don't worry it's getting on a long enough todo list that I won't get around to doing it before the port is over :upside_down:

[Reid Barton]

Prior discussions include https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/kTop.20is.20CCC/near/200970908

[Sophie Morel]

Yaël Dillies said:

I solved my problem without needing this (see #16976), but I can still try to get cg spaces and compactological spaces into mathlib. Where can I read about the latter? I did not find much online.

https://link.springer.com/chapter/10.1007/BFb0061237
(Should not require an account to download.)
I don't think there's much to read, since compactological spaces don't seem to have made it into the mainstream.

[Johan Commelin]

Shameless plug: https://math.commelin.net/2023/condensed/compactological.pdf
But I agree there isn't that much theory yet.