API/tactic for subspace topology

Stream: Is there code for X?

[Winston Yin (尹維晨)]

I had to prove something like:

example (s t : Set ℝ) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  rw [← Subtype.image_preimage_val, ← Subtype.image_preimage_val,
    image_subset_image_iff Subtype.val_injective]
  intros t ht
  rw [mem_preimage, ← closure_subtype] at ht
  revert ht t
  apply IsClosed.closure_subset
  -- goal state: `IsClosed (Subtype.val ⁻¹' s)`
  sorry

In informal mathematics, you would just get to this point by saying "it suffices to show that s ∩ t is closed in the subspace topology of t". Here, I had to finagle the goal into that form by some incantations that are not very discoverable, with all this subtype stuff that's foreign to people who just want to do some analysis.

Is this an inevitable consequence of using type theory, or can we come up with a way to improve user experience when doing point set topology? What would it take, a duplicate API for intersecting with subtypes or writing some new tactic? Maybe something easier already exists in Mathlib?

[Utensil Song]

import Mathlib

example (s t : Set ℝ) (hs : IsClosed s) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  simp only [Set.subset_inter_iff, Set.inter_subset_right, and_true]
  intro x hx
  obtain ⟨hxst, hxt⟩ := hx
  have hsub : closure (s ∩ t) ⊆ s := by
    rw [propext (IsClosed.closure_subset_iff hs)]
    exact Set.inter_subset_left s t
  exact hsub hxst

I don't seem to need to touch subtype stuff during the proof. (I added IsClosed as it seems that I need it for the statement to be true )

[Winston Yin (尹維晨)]

In my case, s is not actually closed. It's s ∩ t that is closed in the subspace topology of t

[Utensil Song]

import Mathlib

example (s t : Set ℝ) (hst: IsClosed (s ∩ t)) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  simp only [Set.subset_inter_iff, Set.inter_subset_right, and_true]
  intro x hx
  obtain ⟨hxst, _⟩ := hx
  have h : (s ∩ t) ⊆ s := by exact Set.inter_subset_left s t
  have hsub : closure (s ∩ t) ⊆ (s ∩ t) := by
    rw [propext (IsClosed.closure_subset_iff hst)]
  exact h (hsub hxst)
  done

Do you mean this? Can you make a #mwe ? It doesn't seem that IsClosed (s ∩ t) can be deduced from other hypotheses, only that IsClosed (closure (s ∩ t)).

[Andrew Yang]

I believe he meant IsClosed (Subtype.val ⁻¹' s : Set t)

[Andrew Yang]

import Mathlib

variable {X} [TopologicalSpace X] (t : Set X)

example (s t : Set X) (hs : IsClosed (Subtype.val ⁻¹' s : Set t)) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  suffices : closure (Subtype.val ⁻¹' s : Set t) ⊆ (Subtype.val ⁻¹' s : Set t)
  · convert Set.image_subset Subtype.val this <;> simp [embedding_subtype_val.closure_eq_preimage_closure_image]
  rwa [IsClosed.closure_subset_iff]

[Utensil Song]

I thought that from the "suffices" up there, he doesn't like to see anything Subtype, particularly not in hypotheses.

[Utensil Song]

At any rate, the proof needs something to be closed, but it's not given in the intial code.

[Andrew Yang]

However IsClosed (s ∩ t) is stronger than IsClosed (Subtype.val ⁻¹' s : Set t) and the equivalent without subtypes is probably ∃ s', IsClosed s' ∧ s ∩ t = s' ∩ t.

[Miguel Marco]

I did find that kind of problem when formalizing my general topology course, so I had to create my own API for that. For convenience, I did create an operation ↓∩ to convert a set of the universe, to a set in a subtype by intersecting it, and then prove the lemmas I need for that subspace topology (many of them are marked as simp for convenience).

It is in Lean3, but porting it to Lean4 should be straightforward. It also uses spanish names... I hope that is not a problem.
Check it here:
https://github.com/miguelmarco/topologia_general_lean/blob/master/subconjuntos.lean
and here
https://github.com/miguelmarco/topologia_general_lean/blob/master/subespacios.lean

[Winston Yin (尹維晨)]

Utensil Song said:

I thought that from the "suffices" up there, he doesn't like to see anything Subtype, particularly not in hypotheses.

Apologies for being a bit unclear. I want Lean to be able to apply IsClosed.closure_subset nearly directly to a goal closure (s ∩ t) ∩ t ⊆ s ∩ t to turn it into IsClosed (Subtype.val ⁻¹' s), by specifying that we are working in the subspace topology of t.

[Winston Yin (尹維晨)]

If I hadn't learnt much type theory, I would not have thought that Subtype.val has anything to do with the original goal at hand, and would have overlooked all the Subtype lemmas. Being able to transform the goal from ... ∩ t to the corresponding statement explicitly mentioning Subtype.val cues the user to now look for and apply Subtype.val lemmas.

[Winston Yin (尹維晨)]

@Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

[Miguel Marco]

Winston Yin (尹維晨) said:

Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

I coinsidered trying to add it,but wasn't sure it would be a good fit. Subspace topology is treated in Mathlib as a particular case of inverse image topology, so there is no real need for that. But maybe other parts of Mathlib could find this kind of API useful. :man_shrugging:

[Andrew Yang]

I do think such a definition would be useful. We also have docs#Subgroup.subgroupOf for example.

[Winston Yin (尹維晨)]

I’d wager that Subtype.val is a pretty good special case of a continuous function, especially when I don’t think about it when dealing with topology within subsets.

[Utensil Song]

Subtype.val should be considered an implementation detail during constructing a mathematical construct. All later interactions with the mathematical construct should be via API lemmas that make sense in math too. This doesn't just happen to Subtype or dependent type theory based ITPs, it also happens in Math, e.g. Clifford Algebra can be constructed by a quotient of Tensor Algebra, so in Lean it could be chosen for the definition, but we throw that detail away once its universal properties are defined, and use only those lemmas afterward, as much as possible.

[Utensil Song]

The concept of lemma APIs are also discussed and explained here recently.

[Miguel Marco]

Andrew Yang said:

I do think such a definition would be useful. We also have docs#Subgroup.subgroupOf for example.

What would be the right place for it?

[Utensil Song]

Miguel Marco said:

Winston Yin (尹維晨) said:

Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

I coinsidered trying to add it,but wasn't sure it would be a good fit. Subspace topology is treated in Mathlib as a particular case of inverse image topology, so there is no real need for that. But maybe other parts of Mathlib could find this kind of API useful. :man_shrugging:

Where is inverse image topology in Mathlib? Can (hs : IsClosed (Subtype.val ⁻¹' s : Set t) be encoding by it and use lemmas there for this proof? With your code it can be encoded as (hs : IsClosed (restringe t s)) and use your lemmas (it seems to need a little more for the closure).

[Jireh Loreaux]

docs#TopologicalSpace.induced

[Jireh Loreaux]

The topology on a set (viewed as a type), is the topology induced by Subtype.val.

[Utensil Song]

Searching on moogle using "​preimage topology" didn't give me docs#TopologicalSpace.induced on the first page :joy: but it's in the doc string.

[Miguel Marco]

I only proved the API lemmas I needed for the theorems we prove in my course, so my API is not as complete as it could be.
Shouldn't be hard to extend it though.