feat(data/set/basic): inclusion map (#906)

* feat(data/set/basic): inclusion map

* add continuous_inclusion

* minor style change

Author: ChrisHughes24

src/data/set/basic.lean

@@ -1264,4 +1264,24 @@ end
 
 end pi
 
+section inclusion
+variable {α : Type*}
+
+/-- `inclusion` is the "identity" function between two subsets `s` and `t`, where `s ⊆ t` -/
+def inclusion {s t : set α} (h : s ⊆ t) : s → t :=
+λ x : s, (⟨x, h x.2⟩ : t)
+
+@[simp] lemma inclusion_self {s : set α} (x : s) :
+  inclusion (set.subset.refl _) x = x := by cases x; refl
+
+@[simp] lemma inclusion_inclusion {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 {s t : set α} (h : s ⊆ t) :
+  function.injective (inclusion h)
+| ⟨_, _⟩ ⟨_, _⟩ := subtype.ext.2 ∘ subtype.ext.1
+
+end inclusion
+
 end set

src/topology/constructions.lean

@@ -388,6 +388,9 @@ lemma continuous_subtype_mk {f : β → α}
   (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
 continuous_induced_rng h
 
+lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) := 
+continuous_subtype_mk _ continuous_subtype_val
+
 lemma continuous_at_subtype_val [topological_space α] {p : α → Prop} {a : subtype p} :
   continuous_at subtype.val a :=
 continuous_iff_continuous_at.mp continuous_subtype_val _