## Stream: maths

### Topic: open_embedding

#### Kevin Buzzard (Apr 23 2019 at 17:38):

Should open_embedding (an open map which is an embedding) be a class? I want to prove ten things about open embeddings and define some comap stuff (pulling back a bunch of structures along open embeddings). Currently I have this:

import topology.maps

class open_embedding {α : Type*} {β : Type*} [topological_space α] [topological_space β]
(f : α → β) : Prop :=
(Hopen : is_open_map f)
(Hembedding : embedding f)


But then I remember that in core Lean things like bijective f is not defined as a class at all, it's just injective f \and surjective f. Which is the best approach? What will make things easier later on?

#### Kevin Buzzard (Apr 23 2019 at 17:41):

I think this is the Stricklandization of the inclusion of an open subset of alpha into alpha

#### Johan Commelin (Apr 23 2019 at 18:15):

Note that you could also have other hypotheses, like

• is_open (set.range f) and embedding f, or
• is_open_map f and injective f and continuous f
So we will likely want several constructors

Last updated: May 18 2021 at 08:14 UTC