feat(topology): tiny new lemmas (#7554)

from LTE





Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/order/filter/bases.lean

@@ -218,6 +218,12 @@ def filter_basis.of_sets (s : set (set α)) : filter_basis α :=
 lemma has_basis.mem_iff (hl : l.has_basis p s) : t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
 hl.mem_iff' t
 
+lemma has_basis.eq_of_same_basis (hl : l.has_basis p s) (hl' : l'.has_basis p s) : l = l' :=
+begin
+  ext t,
+  rw [hl.mem_iff, hl'.mem_iff]
+end
+
 lemma has_basis_iff : l.has_basis p s ↔ ∀ t, t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
 ⟨λ ⟨h⟩, h, λ h, ⟨h⟩⟩
 

src/topology/constructions.lean

@@ -64,6 +64,10 @@ instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_spac
 instance ulift.topological_space [t : topological_space α] : topological_space (ulift.{v u} α) :=
 t.induced ulift.down
 
+lemma quotient.preimage_mem_nhds [topological_space α] [s : setoid α]
+  {V : set $ quotient s} {a : α} (hs : V ∈ 𝓝 (quotient.mk a)) : quotient.mk ⁻¹' V ∈ 𝓝 a :=
+preimage_nhds_coinduced hs
+
 /-- The image of a dense set under `quotient.mk` is a dense set. -/
 lemma dense.quotient [setoid α] [topological_space α] {s : set α} (H : dense s) :
   dense (quotient.mk '' s) :=

src/topology/order.lean

@@ -294,6 +294,14 @@ lemma is_open_coinduced {t : topological_space α} {s : set β} {f : α → β}
   @is_open β (topological_space.coinduced f t) s ↔ is_open (f ⁻¹' s) :=
 iff.rfl
 
+lemma preimage_nhds_coinduced [topological_space α] {π : α → β} {s : set β}
+  {a : α} (hs : s ∈ @nhds β (topological_space.coinduced π ‹_›) (π a)) : π ⁻¹' s ∈ 𝓝 a :=
+begin
+  letI := topological_space.coinduced π ‹_›,
+  rcases mem_nhds_sets_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩,
+  exact mem_nhds_sets_iff.mpr ⟨π ⁻¹' V, set.preimage_mono hVs, V_op, mem_V⟩
+end
+
 variables {t t₁ t₂ : topological_space α} {t' : topological_space β} {f : α → β} {g : β → α}
 
 lemma continuous.coinduced_le (h : @continuous α β t t' f) :