feat(topology): assorted topological lemmas (#3619)

from the sphere eversion project



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/set/basic.lean

@@ -851,9 +851,12 @@ theorem nonempty_diff {s t : set α} : (s \ t).nonempty ↔ ¬ (s ⊆ t) :=
 ⟨λ ⟨x, xs, xt⟩, not_subset.2 ⟨x, xs, xt⟩,
   λ h, let ⟨x, xs, xt⟩ := not_subset.1 h in ⟨x, xs, xt⟩⟩
 
-theorem union_diff_cancel {s t : set α} (h : s ⊆ t) : s ∪ (t \ s) = t :=
+theorem union_diff_cancel' {s t u : set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) : t ∪ (u \ s) = u :=
 by finish [ext_iff, iff_def, subset_def]
 
+theorem union_diff_cancel {s t : set α} (h : s ⊆ t) : s ∪ (t \ s) = t :=
+union_diff_cancel' (subset.refl s) h
+
 theorem union_diff_cancel_left {s t : set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ s = t :=
 by finish [ext_iff, iff_def, subset_def]
 
@@ -1688,6 +1691,9 @@ begin
   rw [image_preimage_eq_of_subset], exact hs₂, rw [range_coe], exact hs₁
 end
 
+lemma preimage_coe_nonempty {s t : set α} : ((coe : s → α) ⁻¹' t).nonempty ↔ (s ∩ t).nonempty :=
+by rw [inter_comm, ← image_preimage_coe, nonempty_image_iff]
+
 end subtype
 
 namespace set

src/order/filter/bases.lean

@@ -213,6 +213,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_iff : l.has_basis p s ↔ ∀ t, t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
+⟨λ ⟨h⟩, h, λ h, ⟨h⟩⟩
+
+lemma has_basis.ex_mem (h : l.has_basis p s) : ∃ i, p i :=
+let ⟨i, pi, h⟩ := h.mem_iff.mp univ_mem_sets in ⟨i, pi⟩
+
 protected lemma is_basis.has_basis (h : is_basis p s) : has_basis h.filter p s :=
 ⟨λ t, by simp only [h.mem_filter_iff, exists_prop]⟩
 
@@ -253,20 +259,23 @@ lemma basis_sets (l : filter α) : l.has_basis (λ s : set α, s ∈ l) id :=
 
 lemma has_basis_self {l : filter α} {P : set α → Prop} :
   has_basis l (λ s, s ∈ l ∧ P s) id ↔ ∀ t, (t ∈ l ↔ ∃ r ∈ l, P r ∧ r ⊆ t) :=
+by simp only [has_basis_iff, exists_prop, id, and_assoc]
+
+/-- If `{s i | p i}` is a basis of a filter `l` and `V ∈ l`, then `{s i | p i ∧ s i ⊆ V}`
+is a basis of `l`. -/
+lemma has_basis.restrict (h : l.has_basis p s) {V : set α} (hV : V ∈ l) :
+  l.has_basis (λ i, p i ∧ s i ⊆ V) s :=
 begin
-  split,
-  { rintros ⟨h⟩ t,
-    convert h t,
-    ext s,
-    tauto, },
-  { intro h,
-    constructor,
-    intro t,
-    convert h t,
-    ext s,
-    tauto }
+  refine ⟨λ t, ⟨λ ht, _, λ ⟨i, hpi, hti⟩, h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩,
+  rcases h.mem_iff.1 (inter_mem_sets hV ht) with ⟨i, hpi, hti⟩,
+  rw subset_inter_iff at hti,
+  exact ⟨i, ⟨hpi, hti.1⟩, hti.2⟩
 end
 
+lemma has_basis.has_basis_self_subset {p : set α → Prop} (h : l.has_basis (λ s, s ∈ l ∧ p s) id)
+  {V : set α} (hV : V ∈ l) : l.has_basis (λ s, s ∈ l ∧ p s ∧ s ⊆ V) id :=
+by simpa only [and_assoc] using h.restrict hV
+
 theorem has_basis.ge_iff (hl' : l'.has_basis p' s')  : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
 ⟨λ h i' hi', h $ hl'.mem_of_mem hi',
   λ h s hs, let ⟨i', hi', hs⟩ := hl'.mem_iff.1 hs in mem_sets_of_superset (h _ hi') hs⟩

src/order/filter/basic.lean

@@ -380,6 +380,9 @@ we use a typeclass argument in lemmas instead. -/
 
 lemma ne_bot.ne {f : filter α} (hf : ne_bot f) : f ≠ ⊥ := hf
 
+@[simp] lemma not_ne_bot {α : Type*} {f : filter α} : ¬ f.ne_bot ↔ f = ⊥ :=
+not_not
+
 lemma ne_bot.mono {f g : filter α} (hf : ne_bot f) (hg : f ≤ g) : ne_bot g :=
 ne_bot_of_le_ne_bot hf hg
 
@@ -1507,6 +1510,17 @@ le_antisymm
   map_comap_le
   (assume t' ⟨t, ht, sub⟩, by filter_upwards [ht, hf]; rintros x hxt ⟨y, rfl⟩; exact sub hxt)
 
+lemma image_mem_sets {f : filter α} {c : β → α} (h : range c ∈ f) {W : set β}
+  (W_in : W ∈ comap c f) : c '' W ∈ f :=
+begin
+  rw ← map_comap h,
+  exact image_mem_map W_in
+end
+
+lemma image_coe_mem_sets {f : filter α} {U : set α} (h : U ∈ f) {W : set U}
+  (W_in : W ∈ comap (coe : U → α) f) : coe '' W ∈ f :=
+image_mem_sets (by simp [h]) W_in
+
 lemma comap_map {f : filter α} {m : α → β} (h : ∀ x y, m x = m y → x = y) :
   comap m (map m f) = f :=
 have ∀s, preimage m (image m s) = s,

src/topology/basic.lean

@@ -422,6 +422,12 @@ begin
   rwa [inter_diff_self, subset_empty_iff] at this,
 end
 
+lemma closure_eq_interior_union_frontier (s : set α) : closure s = interior s ∪ frontier s :=
+(union_diff_cancel interior_subset_closure).symm
+
+lemma closure_eq_self_union_frontier (s : set α) : closure s = s ∪ frontier s :=
+(union_diff_cancel' interior_subset subset_closure).symm
+
 /-!
 ### Neighborhoods
 -/
@@ -705,6 +711,9 @@ lemma is_closed_iff_cluster_pt {s : set α} : is_closed s ↔ ∀a, cluster_pt a
 calc is_closed s ↔ closure s ⊆ s : closure_subset_iff_is_closed.symm
   ... ↔ (∀a, cluster_pt a (𝓟 s) → a ∈ s) : by simp only [subset_def, mem_closure_iff_cluster_pt]
 
+lemma is_closed_iff_nhds {s : set α} : is_closed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).nonempty) → x ∈ s :=
+by simp_rw [is_closed_iff_cluster_pt, cluster_pt, inf_principal_ne_bot_iff]
+
 lemma closure_inter_open {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
 assume a ⟨hs, ht⟩,
 have s ∈ 𝓝 a, from mem_nhds_sets h hs,

src/topology/order.lean

@@ -432,6 +432,11 @@ lemma continuous_induced_rng {g : γ → α} {t₂ : tspace β} {t₁ : tspace 
   (h : cont t₁ t₂ (f ∘ g)) : cont t₁ (induced f t₂) g :=
 assume s ⟨t, ht, s_eq⟩, s_eq ▸ h t ht
 
+lemma continuous_induced_rng' [topological_space α] [topological_space β] [topological_space γ]
+  {g : γ → α} (f : α → β) (H : ‹topological_space α› = ‹topological_space β›.induced f)
+  (h : continuous (f ∘ g)) : continuous g :=
+H.symm ▸ continuous_induced_rng h
+
 lemma continuous_coinduced_rng {t : tspace α} : cont t (coinduced f t) f :=
 assume s h, h
 

src/topology/subset_properties.lean

@@ -1004,6 +1004,9 @@ that contains this point. -/
 def connected_component (x : α) : set α :=
 ⋃₀ { s : set α | is_preconnected s ∧ x ∈ s }
 
+/-- The connected component of a point inside a set. -/
+def connected_component_in (F : set α) (x : F) : set α := coe '' (connected_component x)
+
 theorem mem_connected_component {x : α} : x ∈ connected_component x :=
 mem_sUnion_of_mem (mem_singleton x) ⟨is_connected_singleton.is_preconnected, mem_singleton x⟩
 
@@ -1043,6 +1046,26 @@ end prio
 
 attribute [instance, priority 50] connected_space.to_nonempty -- see Note [lower instance priority]
 
+lemma is_connected_range [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :
+  is_connected (range f) :=
+begin
+  inhabit α,
+  rw ← image_univ,
+  exact ⟨⟨f (default α), mem_image_of_mem _ (mem_univ _)⟩,
+         is_preconnected.image is_preconnected_univ _ h.continuous_on⟩
+end
+
+lemma connected_space_iff_connected_component :
+  connected_space α ↔ ∃ x : α, connected_component x = univ :=
+begin
+  split,
+  { rintros ⟨h, ⟨x⟩⟩,
+    exactI ⟨x, eq_univ_of_univ_subset $ subset_connected_component is_preconnected_univ (mem_univ x)⟩ },
+  { rintros ⟨x, h⟩,
+    haveI : preconnected_space α := ⟨by {rw ← h, exact is_connected_connected_component.2 }⟩,
+    exact ⟨⟨x⟩⟩ }
+end
+
 @[priority 100] -- see Note [lower instance priority]
 instance preirreducible_space.preconnected_space (α : Type u) [topological_space α]
   [preirreducible_space α] : preconnected_space α :=
@@ -1067,6 +1090,10 @@ theorem is_clopen_iff [preconnected_space α] {s : set α} : is_clopen s ↔ s =
   h3 h2,
 by rintro (rfl | rfl); [exact is_clopen_empty, exact is_clopen_univ]⟩
 
+lemma eq_univ_of_nonempty_clopen [preconnected_space α] {s : set α}
+  (h : s.nonempty) (h' : is_clopen s) : s = univ :=
+by { rw is_clopen_iff at h', finish [h.ne_empty] }
+
 lemma subtype.preconnected_space {s : set α} (h : is_preconnected s) :
   preconnected_space s :=
 { is_preconnected_univ :=