Discrete subset of a topological space

Stream: Is there code for X?

[Kevin Buzzard]

Do we have a nice way of saying

(∀ x : X, ∃ U : Set Y, IsOpen U ∧  f⁻¹' U = {x})

where f : X -> Y and Y is a topological space? It's "f is injective and the image is discrete" but we don't seem to have a predicate on subspaces of a topological space to say they get the discrete topology.

[Yaël Dillies]

Injective f ∧ DiscreteTopology (range f)?

[Kevin Buzzard]

A PR to FLT is using this a lot, e.g. "if e : X' Equiv X then true for f iff true for f composed with e" and "if true for f : X -> Y then true for f^n : X^n -> Y^n" etc. It seems a bit weird to set all this up as an "and". Or maybe it doesn't? Should we be doing this?

[Aaron Liu]

if you equip X with the discrete topology (do we have a type synonym for that?) then it's equivalent to saying that f is a docs#Topology.IsEmbedding

[Kevin Buzzard]

But in the application X might be the rationals and I don't really want to go around equipping it with the discrete topology

[Aaron Liu]

that's why I asked for a type synonym

[Yaël Dillies]

Even using a type synonym is probably too much noise

[Aaron Liu]

how about TopologicalSpace.induced f inst = ⊥

[Aaron Liu]

the induced topology is discrete

[Yaël Dillies]

Aaron, we all agree this predicate can be easily written. The question is whether it can easily be used

[Aaron Liu]

how do you want to use it

[Aaron Liu]

I haven't seen a use yet

[Aaron Liu]

maybe if I saw some use cases

[Yaël Dillies]

Kevin, in measure theory we have notations like Measure[m] alpha or Measurable[malpha] f, Measurable[malpha, mbeta] f for when m, ... aren't the canonical instances of MeasurableSpace alpha, ... What about an IsEmbedding[talpha] f notation? Then your predicate is IsEmbedding[\bot] f and you can use all the IsEmbedding API (provided you open some PRs to replace [TopologicalSpace alpha] with {t : TopologicalSpace alpha} in a bunch of places, which is what I routinely do in measure land).

[Anatole Dedecker]

This does not answer Kevin's question, but mathematically I agree with Aaron that the best way to think of this is as an embedding from X with the discrete topology