feat(topology): add a few lemmas (#9885)

Add `is_topological_basis.is_open_map_iff`,
`is_topological_basis.exists_nonempty_subset`, and
`interior_{s,b,}Inter_subset`.

Motivated by lemmas from `flypitch`.

src/topology/bases.lean

@@ -167,6 +167,25 @@ begin
   exact ⟨λ h o hb ⟨a, ha⟩, h a o hb ha, λ h a o hb ha, h o hb ⟨a, ha⟩⟩
 end
 
+lemma is_topological_basis.is_open_map_iff {β} [topological_space β] {B : set (set α)}
+  (hB : is_topological_basis B) {f : α → β} :
+  is_open_map f ↔ ∀ s ∈ B, is_open (f '' s) :=
+begin
+  refine ⟨λ H o ho, H _ (hB.is_open ho), λ hf o ho, _⟩,
+  rw [hB.open_eq_sUnion' ho, sUnion_eq_Union, image_Union],
+  exact is_open_Union (λ s, hf s s.2.1)
+end
+
+lemma is_topological_basis.exists_nonempty_subset {B : set (set α)}
+  (hb : is_topological_basis B) {u : set α} (hu : u.nonempty) (ou : is_open u) :
+  ∃ v ∈ B, set.nonempty v ∧ v ⊆ u :=
+begin
+  cases hu with x hx,
+  rw [hb.open_eq_sUnion' ou, mem_sUnion] at hx,
+  rcases hx with ⟨v, hv, hxv⟩,
+  exact ⟨v, hv.1, ⟨x, hxv⟩, hv.2⟩
+end
+
 lemma is_topological_basis_opens : is_topological_basis { U : set α | is_open U } :=
 is_topological_basis_of_open_of_nhds (by tauto) (by tauto)
 

src/topology/basic.lean

@@ -303,8 +303,19 @@ subset.antisymm
 lemma is_open_iff_forall_mem_open : is_open s ↔ ∀ x ∈ s, ∃ t ⊆ s, is_open t ∧ x ∈ t :=
 by rw ← subset_interior_iff_open; simp only [subset_def, mem_interior]
 
+lemma interior_Inter_subset (s : ι → set α) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) :=
+subset_Inter $ λ i, interior_mono $ Inter_subset _ _
+
+lemma interior_bInter_subset (p : ι → Sort*) (s : Π i, p i → set α) :
+  interior (⋂ i (hi : p i), s i hi) ⊆ ⋂ i (hi : p i), interior (s i hi) :=
+(interior_Inter_subset _).trans $ Inter_subset_Inter $ λ i, interior_Inter_subset _
+
+lemma interior_sInter_subset (S : set (set α)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s :=
+calc interior (⋂₀ S) = interior (⋂ s ∈ S, s) : by rw sInter_eq_bInter
+                 ... ⊆ ⋂ s ∈ S, interior s  : interior_bInter_subset _ _
+
 /-!
-### Closure of a set
+### Closure of a set
 -/
 
 /-- The closure of `s` is the smallest closed set containing `s`. -/