feat(topology/opens): open_embedding_of_le (#3597)

Add `lemma open_embedding_of_le {U V : opens α} (i : U ≤ V) : open_embedding (set.inclusion i)`.

Also, I was finding it quite inconvenient to have `x ∈ U` for `U : opens X` being unrelated to `x ∈ (U : set X)`. I propose we just add the simp lemmas in this PR that unfold to the set-level membership operation.

(I'd be happy to go the other way if someone has a strong opinion here; just that we pick a simp normal form for talking about membership and inclusion of opens.)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/topology/opens.lean

@@ -44,6 +44,10 @@ instance : has_subset (opens α) :=
 instance : has_mem α (opens α) :=
 { mem := λ a U, a ∈ (U : set α) }
 
+@[simp] lemma subset_coe {U V : opens α} : ((U : set α) ⊆ (V : set α)) = (U ⊆ V) := rfl
+
+@[simp] lemma mem_coe {x : α} {U : opens α} : (x ∈ (U : set α)) = (x ∈ U) := rfl
+
 @[ext] lemma ext {U V : opens α} (h : (U : set α) = V) : U = V := subtype.ext_iff.mpr h
 
 @[ext] lemma ext_iff {U V : opens α} : (U : set α) = V ↔ U = V :=
@@ -107,6 +111,22 @@ end
 lemma supr_def {ι} (s : ι → opens α) : (⨆ i, s i) = ⟨⋃ i, s i, is_open_Union $ λ i, (s i).2⟩ :=
 by { ext, simp only [supr, opens.Sup_s, sUnion_image, bUnion_range], refl }
 
+@[simp] lemma supr_s {ι} (s : ι → opens α) : ((⨆ i, s i : opens α) : set α) = ⋃ i, s i :=
+by simp [supr_def]
+
+theorem mem_supr {ι} {x : α} {s : ι → opens α} : x ∈ supr s ↔ ∃ i, x ∈ s i :=
+by { rw [←mem_coe], simp, }
+
+lemma open_embedding_of_le {U V : opens α} (i : U ≤ V) :
+  open_embedding (set.inclusion i) :=
+{ inj := set.inclusion_injective i,
+  induced := (@induced_compose _ _ _ _ (set.inclusion i) coe).symm,
+  open_range :=
+  begin
+    rw set.range_inclusion i,
+    exact continuous_subtype_val U.val U.property
+  end, }
+
 def is_basis (B : set (opens α)) : Prop := is_topological_basis ((coe : _ → set α) '' B)
 
 lemma is_basis_iff_nbhd {B : set (opens α)} :
@@ -197,9 +217,3 @@ instance open_nhds_of.inhabited {α : Type*} [topological_space α] (x : α) :
   inhabited (open_nhds_of x) := ⟨⟨set.univ, is_open_univ, set.mem_univ _⟩⟩
 
 end topological_space
-
-namespace continuous
-open topological_space
-
-
-end continuous