Zulip Chat Archive

Stream: maths

Topic: inclusions of subtype.topological_space


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 08 2019 at 23:09):

I guess use embedding_subtype_val and embedding.continuous_iff in some fashion

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 08 2019 at 23:15):

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

view this post on Zulip Reid Barton (Apr 08 2019 at 23:19):

Oh yeah, that's easier

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 08 2019 at 23:28):

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

view this post on Zulip 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