feat(topology): path connected spaces (#3627)

From the sphere eversion project.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/data/set/intervals/basic.lean

@@ -58,6 +58,22 @@ def Ici (a : α) := {x | a ≤ x}
 /-- Left-open right-infinite interval -/
 def Ioi (a : α) := {x | a < x}
 
+lemma Ioo_def (a b : α) : {x | a < x ∧ x < b} = Ioo a b := rfl
+
+lemma Ico_def (a b : α) : {x | a ≤ x ∧ x < b} = Ico a b := rfl
+
+lemma Iio_def (a : α) : {x | x < a} = Iio a := rfl
+
+lemma Icc_def (a b : α) : {x | a ≤ x ∧ x ≤ b} = Icc a b := rfl
+
+lemma Iic_def (b : α) : {x | x ≤ b} = Iic b := rfl
+
+lemma Ioc_def (a b : α) : {x | a < x ∧ x ≤ b} = Ioc a b := rfl
+
+lemma Ici_def (a : α) : {x | a ≤ x} = Ici a := rfl
+
+lemma Ioi_def (a : α) : {x | a < x} = Ioi a := rfl
+
 @[simp] lemma mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b := iff.rfl
 @[simp] lemma mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b := iff.rfl
 @[simp] lemma mem_Iio : x ∈ Iio b ↔ x < b := iff.rfl

src/geometry/manifold/real_instances.lean

@@ -378,7 +378,4 @@ local attribute [instance] fact_zero_lt_one
 instance : charted_space (euclidean_half_space 1) (Icc (0 : ℝ) 1) := by apply_instance
 instance : smooth_manifold_with_corners (𝓡∂ 1) (Icc (0 : ℝ) 1) := by apply_instance
 
-instance : has_zero (Icc (0 : ℝ) 1) := ⟨⟨(0 : ℝ), ⟨le_refl _, zero_le_one⟩⟩⟩
-instance : has_one (Icc (0 : ℝ) 1) := ⟨⟨(1 : ℝ), ⟨zero_le_one, le_refl _⟩⟩⟩
-
 end

src/order/filter/bases.lean

@@ -244,6 +244,23 @@ by erw [(filter_basis.of_sets s).generate, ← (has_basis_generate s).filter_eq]
 lemma of_sets_filter_eq_generate (s : set (set α)) : (filter_basis.of_sets s).filter = generate s :=
 by rw [← (filter_basis.of_sets s).generate, generate_eq_generate_inter s] ; refl
 
+lemma has_basis.to_has_basis (hl : l.has_basis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
+  (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l.has_basis p' s' :=
+begin
+  constructor,
+  intro t,
+  rw hl.mem_iff,
+  split,
+  { rintros ⟨i, pi, hi⟩,
+    rcases h i pi with ⟨i', pi', hi'⟩,
+    use [i', pi'],
+    tauto },
+  { rintros ⟨i', pi', hi'⟩,
+    rcases h' i' pi' with ⟨i, pi, hi⟩,
+    use [i, pi],
+    tauto },
+end
+
 lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} :
   (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x :=
 by simpa using hl.mem_iff