# Zulip Chat Archive

## Stream: maths

### Topic: inclusions of subtype.topological_space

#### Scott Morrison (Apr 08 2019 at 23:00):

Say I have `U V : set A`

, and `topological_space A`

, and `h : U \subseteq V`

.

How do I get the continuity of the inclusion between the `subtype.topological_space`

instances for `U`

and `V`

?

#### Scott Morrison (Apr 08 2019 at 23:00):

I can't find this in mathlib, but I'm not too familiar with the topology files.

#### Reid Barton (Apr 08 2019 at 23:09):

I guess use `embedding_subtype_val`

and `embedding.continuous_iff`

in some fashion

#### Chris Hughes (Apr 08 2019 at 23:15):

import topology.constructions def inclusion {α : Type*} {s t : set α} (h : s ⊆ t) : s → t := λ x : s, (⟨x, h x.2⟩ : t) @[simp] lemma inclusion_self {α : Type*} {s : set α} (h : s ⊆ s) (x : s) : inclusion h x = x := by cases x; refl @[simp] lemma inclusion_inclusion {α : Type*} {s t u : set α} (hst : s ⊆ t) (htu : t ⊆ u) (x : s) : inclusion htu (inclusion hst x) = inclusion (set.subset.trans hst htu) x := by cases x; refl lemma inclusion_injective {α : Type*} {s t : set α} (h : s ⊆ t) : function.injective (inclusion h) | ⟨_, _⟩ ⟨_, _⟩ := subtype.ext.2 ∘ subtype.ext.1 example {α : Type*} [topological_space α] (s t : set α) (h : s ⊆ t) : continuous (inclusion h) := continuous_subtype_mk _ continuous_subtype_val

#### Chris Hughes (Apr 08 2019 at 23:15):

Do we want the `inclusion`

function in mathlib. I wrote it for something else

#### Reid Barton (Apr 08 2019 at 23:19):

Oh yeah, that's easier

#### Scott Morrison (Apr 08 2019 at 23:27):

I got it to work with `(embedding.continuous_iff embedding_subtype_val).2 continuous_induced_dom`

, thanks @Reid Barton.

#### Scott Morrison (Apr 08 2019 at 23:28):

But yes, @Chris Hughes, let's definitely have your version!

#### Scott Morrison (Apr 08 2019 at 23:32):

@Chris Hughes, can you just add the last `example`

to your PR, as well? That's the one I actually want, and there's not point having me write `continuous_subtype_mk _ continuous_subtype_val`

. :-)

Last updated: May 09 2021 at 10:11 UTC