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