Equip a type with the discrete topology

Stream: Is there code for X?

[Matthias U]

I'd like to reason about bounded functions G -> ℝ, where G is a group. Equivalently, theses are bounded continuous functions G -> ℝ if we equip G with the discrete topology.

So far, I tried the following:

import topology.continuous_function.bounded
import topology.category.Top

open bounded_continuous_function

variables (G : Type*) [group G]

instance : topological_space G := ⊥
instance : discrete_topology G := ⟨rfl⟩

def foo : bounded_continuous_function G ℝ
        := bounded_continuous_function.const G (1:ℝ)

In the line instance : topological_space G := ⊥, I get the message "invalid definition, a declaration named 'topological_space' has already been declared", however, if I remove it, the compiler fails to synthesize the type class instance for topological space G.

How can I equip the group G with the discrete topology?

[Johan Commelin]

@Matthias U You need to give it a name explicitly, e.g. instance foobar : topo...

[Johan Commelin]

However, when you try to apply these results, it might be better to do

variables (G : Type*) [group G] [topological_space G] [discrete_topology G]

[Johan Commelin]

That way you assume that G has a discrete topology, without requiring it to be \bot by definition. (It will of course still be equal to \bot by assumption.

[Matthias U]

that works, thanks .

[Anne Baanen]

In addition, those instances essentially "for all groups G, G has a canonical topology, namely the discrete one", while putting it in a variable means "let G be a group and assume it has the discrete topology"

[Anne Baanen]

So the instances will prevent you from working with other topological groups

[Sebastien Gouezel]

In https://github.com/leanprover-community/mathlib/blob/master/counterexamples/phillips.lean, I need to put the discrete topology on the real line. Here I use a type synonym discrete_copy. If it is useful for you, this could be moved to the src directory.

[Matthias U]

@Anne Baanen ok, I see

[Matthias U]

@Sebastien Gouezel thanks