inclusions of subtype.topological_space

Stream: maths

[Scott Morrison]

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]

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

[Reid Barton]

I guess use embedding_subtype_val and embedding.continuous_iff in some fashion

[Chris Hughes]

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]

Do we want the inclusion function in mathlib. I wrote it for something else

[Reid Barton]

Oh yeah, that's easier

[Scott Morrison]

I got it to work with (embedding.continuous_iff embedding_subtype_val).2 continuous_induced_dom, thanks @Reid Barton.

[Scott Morrison]

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

[Scott Morrison]

@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. :-)