Reorganized the code

src/data/set/basic.lean

@@ -1206,11 +1206,11 @@ rfl
 
 @[simp] theorem preimage_id' {s : set α} : (λ x, x) ⁻¹' s = s := rfl
 
-theorem preimage_const_of_mem {b : β} {s : set β} (h : b ∈ s) :
+@[simp] theorem preimage_const_of_mem {b : β} {s : set β} (h : b ∈ s) :
   (λ (x : α), b) ⁻¹' s = univ :=
 eq_univ_of_forall $ λ x, h
 
-theorem preimage_const_of_not_mem {b : β} {s : set β} (h : b ∉ s) :
+@[simp] theorem preimage_const_of_not_mem {b : β} {s : set β} (h : b ∉ s) :
   (λ (x : α), b) ⁻¹' s = ∅ :=
 eq_empty_of_subset_empty $ λ x hx, h hx
 

src/topology/constructions.lean

@@ -131,6 +131,9 @@ continuous_snd.continuous_at
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
 continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
 
+@[continuity] lemma continuous.prod.mk (a : α) : continuous (prod.mk a : β → α × β) :=
+continuous_const.prod_mk continuous_id'
+
 lemma continuous.prod_map {f : γ → α} {g : δ → β} (hf : continuous f) (hg : continuous g) :
   continuous (λ x : γ × δ, (f x.1, g x.2)) :=
 (hf.comp continuous_fst).prod_mk (hg.comp continuous_snd)

src/topology/local_homeomorph.lean

@@ -209,6 +209,15 @@ lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
 e.symm.source_inter_preimage_inv_preimage _
 
+lemma source_inter_preimage_target_inter (s : set β) :
+  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
+begin
+  refine ext_iff.mpr (λ x, ⟨λ hx, _, λ hx, _⟩),
+  simp only [mem_inter_eq, mem_preimage] at *;
+  exact ⟨hx.1, hx.2.2⟩,
+  exact ⟨hx.1, e.to_local_equiv.map_source hx.1, hx.2⟩, --exacts?
+end
+
 /-- Two local homeomorphisms are equal when they have equal `to_fun`, `inv_fun` and `source`.
 It is not sufficient to have equal `to_fun` and `source`, as this only determines `inv_fun` on
 the target. This would only be true for a weaker notion of equality, arguably the right one,

src/topology/order.lean

@@ -420,6 +420,15 @@ le_antisymm
   (coinduced_le_iff_le_induced.1 $ le_generate_from $ assume s hs,
     generate_open.basic _ $ mem_image_of_mem _ hs)
 
+lemma le_induced_generate {α β} [t : topological_space α] {b : set (set β)}
+  {f : α → β} (h : ∀ (a : set β), a ∈ b → is_open (f ⁻¹' a)) : t ≤ induced f (generate_from b) :=
+begin
+  rw induced_generate_from_eq,
+  apply le_generate_from,
+  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp_distrib],
+  exact h,
+end
+
 /-- This construction is left adjoint to the operation sending a topology on `α`
   to its neighborhood filter at a fixed point `a : α`. -/
 protected def topological_space.nhds_adjoint (a : α) (f : filter α) : topological_space α :=

src/topology/topological_fiber_bundle.lean

@@ -137,14 +137,6 @@ for the initial bundle.
 Fiber bundle, topological bundle, vector bundle, local trivialization, structure group
 -/
 
-section
-
-@[continuity] lemma _root_.continuous.prod.mk {α : Type*} {β : Type*} [topological_space α]
-  [topological_space β] (a : α) : continuous (prod.mk a : β → α × β) :=
-continuous_const.prod_mk continuous_id'
-
-end
-
 variables {ι : Type*} {B : Type*} {F : Type*}
 
 open topological_space filter set
@@ -913,6 +905,10 @@ def local_triv (i : ι) : local_homeomorph Z.total_space (B × F) :=
   end,
   to_local_equiv := Z.local_triv' i }
 
+@[simp] lemma local_triv'_coe (i : ι) : ⇑(Z.local_triv' i) = Z.local_triv i := rfl
+@[simp] lemma local_triv'_source (i : ι) : (Z.local_triv' i).source = (Z.local_triv i).source := rfl
+@[simp] lemma local_triv'_target (i : ι) : (Z.local_triv' i).target = (Z.local_triv i).target := rfl
+
 /- We will now state again the basic properties of the local trivializations, but without primes,
 i.e., for the local homeomorphism instead of the local equiv. -/
 
@@ -957,29 +953,10 @@ Z.is_topological_fiber_bundle.continuous_proj
 lemma is_open_map_proj : is_open_map Z.proj :=
 Z.is_topological_fiber_bundle.is_open_map_proj
 
-/-- Preferred local trivialization of a fiber bundle constructed from core, at a given point, as
-a local homeomorphism -/
-def local_triv_at (p : Z.total_space) :
-  local_homeomorph Z.total_space (B × F) :=
-Z.local_triv (Z.index_at (Z.proj p))
-
-@[simp, mfld_simps] lemma mem_local_triv_at_source (p : Z.total_space) :
-  p ∈ (Z.local_triv_at p).source :=
-by simp [local_triv_at]
-
-@[simp, mfld_simps] lemma local_triv_at_fst (p q : Z.total_space) :
-  ((Z.local_triv_at p) q).1 = q.1 := rfl
-
-@[simp, mfld_simps] lemma local_triv_at_symm_fst (p : Z.total_space) (q : B × F) :
-  ((Z.local_triv_at p).symm q).1 = q.1 := rfl
-
 /-- Preferred local trivialization of a fiber bundle constructed from core, at a given point, as
 a bundle trivialization -/
-def local_triv_at_ext (p : Z.total_space) : bundle_trivialization F Z.proj :=
-Z.local_triv_ext (Z.index_at (Z.proj p))
-
-@[simp, mfld_simps] lemma local_triv_at_ext_to_local_homeomorph (p : Z.total_space) :
-  (Z.local_triv_at_ext p).to_local_homeomorph = Z.local_triv_at p := rfl
+def local_triv_at_ext (b : B) : bundle_trivialization F Z.proj :=
+Z.local_triv_ext (Z.index_at b)
 
 /-- If an element of `F` is invariant under all coordinate changes, then one can define a
 corresponding section of the fiber bundle, which is continuous. This applies in particular to the
@@ -1002,52 +979,44 @@ begin
   { exact A }
 end
 
---lemma la_svaggia (e : local_homeomorph Z (B × F)) {t : set (B × F)} : e ⁻¹' (e.target ∩ t) = e.source ∩ (e ⁻¹' t) := sorry
+variable (i : ι)
 
-@[simp] lemma local_triv'_coe (i : ι) : ⇑(Z.local_triv' i) = Z.local_triv i := rfl
-@[simp] lemma local_triv'_source (i : ι) : (Z.local_triv' i).source = (Z.local_triv i).source := rfl
-@[simp] lemma local_triv'_target (i : ι) : (Z.local_triv' i).target = (Z.local_triv i).target := rfl
-@[simp] lemma local_triv_coe (i : ι) : ⇑(Z.local_triv i) = Z.local_triv_ext i := rfl
-@[simp] lemma local_triv_source (i : ι) : (Z.local_triv i).source = (Z.local_triv_ext i).source := rfl
-@[simp] lemma local_triv_target (i : ι) : (Z.local_triv i).target = (Z.local_triv_ext i).target := rfl
+@[simp] lemma local_triv_coe : ⇑(Z.local_triv i) = Z.local_triv_ext i := rfl
+@[simp] lemma local_triv_source : (Z.local_triv i).source = (Z.local_triv_ext i).source := rfl
+@[simp] lemma local_triv_target : (Z.local_triv i).target = (Z.local_triv_ext i).target := rfl
+@[simp] lemma base_set_at : Z.base_set i = (Z.local_triv_ext i).base_set := rfl
 
-lemma source_target {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  (e : local_homeomorph α β) (s : set β) : e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
-begin
-  refine ext_iff.mpr (λ x, ⟨λ hx, _, λ hx, _⟩),
-  simp only [mem_inter_eq, mem_preimage] at *;
-  exact ⟨hx.1, hx.2.2⟩,
-  exact ⟨hx.1, e.to_local_equiv.map_source hx.1, hx.2⟩, --exacts?
-end
+@[simp, mfld_simps] lemma local_triv_ext_apply (p : Z.total_space) :
+  (Z.local_triv_ext i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
+
+@[simp] lemma local_triv_at_apply (b : B) (a : F): ((Z.local_triv_at_ext b) ⟨b, a⟩) = ⟨b, a⟩ :=
+by { rw [local_triv_at_ext, local_triv_ext_apply, coord_change_self], exact Z.mem_base_set_at b }
 
-@[simp] lemma base_set_at (i : ι) : Z.base_set i = (Z.local_triv_ext i).base_set := rfl
+/-- The inclusion of a fiber into the total space is a continuous map.
 
-lemma continuous_sigma_mk (b : B) : @continuous _ _ _ (Z.to_topological_space ι) -- why does it found the sigma topology instead?
+why does it find the sigma topology instead!? -/
+lemma continuous_sigma_mk (b : B) : @continuous _ _ _ (Z.to_topological_space ι)
   (λ a, (⟨b, a⟩ : (bundle.total_space Z.fiber))) :=
 begin
   rw [continuous_iff_le_induced, topological_fiber_bundle_core.to_topological_space],
-  rw induced_generate_from_eq, --lemma
-  apply le_generate_from,
-  simp only [mem_image, exists_prop, mem_Union, mem_singleton_iff],
-  intros s hs,
-  rcases hs with ⟨_, ⟨i, t, ht, rfl⟩, rfl⟩, --lemma
-  rw [local_triv'_source, local_triv'_coe, ←(source_target Z (Z.local_triv i) t), preimage_inter,
-    ←preimage_comp, local_triv_source, bundle_trivialization.source_eq],
+  apply le_induced_generate,
+  simp only [mem_Union, mem_singleton_iff, local_triv'_source, local_triv'_coe, mem_image],
+  rintros s ⟨i, t, ht, rfl⟩,
+  rw [←(source_inter_preimage_target_inter_eq (Z.local_triv i) t), preimage_inter, ←preimage_comp,
+    local_triv_source, bundle_trivialization.source_eq],
   apply is_open.inter,
   { simp only [bundle.proj, proj, ←preimage_comp],
     by_cases (b ∈ (Z.local_triv_ext i).base_set),
-    { rw preimage_const_of_mem h, --simp
-      exact is_open_univ, },
-    { rw preimage_const_of_not_mem h, --simp
-      exact is_open_empty, }},
+    { rw preimage_const_of_mem h, exact is_open_univ, },
+    { rw preimage_const_of_not_mem h, exact is_open_empty, }},
   { simp only [function.comp, local_triv_apply],
     rw [preimage_comp, local_triv_target],
     by_cases (b ∈ Z.base_set i),
-    { have hc : continuous (λ (x : Z.fiber b), (Z.coord_change (Z.index_at b) i b) x) := by {
+    { have hc : continuous (λ (x : Z.fiber b), (Z.coord_change (Z.index_at b) i b) x) := begin
         rw continuous_iff_continuous_on_univ,
         refine ((Z.coord_change_continuous (Z.index_at b) i).comp ((continuous_const).prod_mk
-        continuous_id).continuous_on) (by { convert (subset_univ univ),
-          exact mk_preimage_prod_right (mem_inter (Z.mem_base_set_at b) h), })},
+          continuous_id).continuous_on) (by { convert (subset_univ univ),
+            exact mk_preimage_prod_right (mem_inter (Z.mem_base_set_at b) h), }) end,
       exact hc.is_open_preimage _ ((continuous.prod.mk b).is_open_preimage _
         ((Z.local_triv i).open_target.inter ht)), },
     { rw [(Z.local_triv_ext i).target_eq, preimage_inter, ←base_set_at,

src/topology/vector_bundle.lean

@@ -267,8 +267,11 @@ iff.rfl
 
 end continuous
 
+/-! ### Constructing topological vector bundles -/
+
 variables (B)
 
+/-- Analogous construction of `topological_fiber_bundle_core` for vector bundles. -/
 @[nolint has_inhabited_instance]
 structure topological_vector_bundle_core (ι : Type*) :=
 (base_set          : ι → set B)
@@ -289,9 +292,9 @@ namespace topological_vector_bundle_core
 variables {R B F} {ι : Type*} [topological_space B] [topological_space F]
 (Z : topological_vector_bundle_core R B F ι)
 
+/-- Natural identification to a `topological_fiber_bundle_core`. -/
 def to_topological_vector_bundle_core : topological_fiber_bundle_core ι B F :=
-{ coord_change := λ i j b, Z.coord_change i j b,
-  ..Z }
+{ coord_change := λ i j b, Z.coord_change i j b, ..Z }
 
 instance to_topological_vector_bundle_core_coe : has_coe (topological_vector_bundle_core R B F ι)
   (topological_fiber_bundle_core ι B F) := ⟨to_topological_vector_bundle_core⟩
@@ -358,72 +361,46 @@ def local_triv (i : ι) : topological_vector_bundle.trivialization R F Z.fiber :
     coe_snd_map_smul, linear_map.map_smul] },
   ..topological_fiber_bundle_core.local_triv_ext ↑Z i }
 
-lemma bbb (i : ι) (b : B) (a : F): ((Z.local_triv i) ⟨b, a⟩) = ⟨b, Z.coord_change (Z.index_at b) i b a⟩ := rfl --generalize
-
-lemma aaa (b : B) (a : F): ((Z.local_triv (Z.index_at b)) ⟨b, a⟩) = ⟨b, a⟩ := --generalize
-begin
-  rw bbb,
-  rw coord_change_self,
-  exact Z.mem_base_set_at b,
-end
-
 @[simp, mfld_simps] lemma mem_local_triv_source (i : ι) (p : total_space Z.fiber) :
   p ∈ (Z.local_triv i).source ↔ p.1 ∈ Z.base_set i :=
 iff.rfl
 
-lemma mem_source_at (b : B) (a : F) :
-  (⟨b, a⟩ : total_space Z.fiber) ∈ (Z.local_triv (Z.index_at b)).source :=
-begin
-  rw mem_local_triv_source,
-  exact Z.mem_base_set_at b,
-end
+/-- Preferred local trivialization of a vector bundle constructed from core, at a given point, as
+a bundle trivialization -/
+def local_triv_at (b : B) : topological_vector_bundle.trivialization R F Z.fiber :=
+Z.local_triv (Z.index_at b)
 
+lemma mem_source_at (b : B) (a : F) :
+  (⟨b, a⟩ : total_space Z.fiber) ∈ (Z.local_triv_at b).source :=
+by { rw [local_triv_at, mem_local_triv_source], exact Z.mem_base_set_at b }
 
+@[simp] lemma local_triv_at_apply (b : B) (a : F): ((Z.local_triv_at b) ⟨b, a⟩) = ⟨b, a⟩ :=
+topological_fiber_bundle_core.local_triv_at_apply Z b a
 
 instance : topological_vector_bundle R F Z.fiber :=
-{
-  inducing := λ b, ⟨by { apply le_antisymm,
-    {
-      rw ←continuous_iff_le_induced,
-      exact topological_fiber_bundle_core.continuous_sigma_mk ↑Z b,
-    },
-    {
-      intro s,
-      intro h,
-      let i := Z.index_at b,
-      refine is_open_induced_iff.mpr ⟨(Z.local_triv i).source ∩ (Z.local_triv i) ⁻¹' (Z.base_set i).prod s, _, _⟩,
-      {
-          exact (continuous_on_open_iff (Z.local_triv i).open_source).mp (Z.local_triv i).continuous_to_fun _ (is_open.prod (Z.is_open_base_set i) h),
-      },
-      {
-        simp only [preimage_inter],
-        rw ←preimage_comp,
-        simp only [function.comp, id.def],
-        ext a,
-        split,
-        {
-          intro ha,
-          simp only [mem_prod, mem_preimage, mem_inter_eq] at ha,
-          rw aaa at ha,
-          exact ha.2.2,
-        },
-        {
-          intro ha,
-          simp only [mem_prod, mem_preimage, mem_inter_eq],
-          split,
-          {
-            exact Z.mem_base_set_at b,
-          },
-          {
-            rw (Z.local_triv i).coe_fst (Z.mem_source_at b a),
-            rw aaa,
-            exact ⟨Z.mem_base_set_at b, ha⟩,
-          }
-        }
-      }
-    }
-  }⟩,
-  locally_trivial := sorry,
-}
+{ inducing := λ b, ⟨ begin refine le_antisymm _ (λ s h, _),
+  { rw ←continuous_iff_le_induced,
+    exact topological_fiber_bundle_core.continuous_sigma_mk ↑Z b, },
+  { refine is_open_induced_iff.mpr ⟨(Z.local_triv_at b).source ∩ (Z.local_triv_at b) ⁻¹'
+      (Z.local_triv_at b).base_set.prod s, (continuous_on_open_iff
+      (Z.local_triv_at b).open_source).mp (Z.local_triv_at b).continuous_to_fun _
+      (is_open.prod (Z.local_triv_at b).open_base_set h), _⟩,
+    rw [preimage_inter, ←preimage_comp],
+    simp only [function.comp, id.def],
+    refine ext_iff.mpr (λ a, ⟨λ ha, _, λ ha, ⟨Z.mem_base_set_at b, _⟩⟩),
+    { simp only [mem_prod, mem_preimage, mem_inter_eq, local_triv_at_apply] at ha,
+      exact ha.2.2, },
+    { simp only [mem_prod, mem_preimage, mem_inter_eq,
+        (Z.local_triv_at b).coe_fst (Z.mem_source_at b a), local_triv_at_apply],
+        exact ⟨Z.mem_base_set_at b, ha⟩, }} end⟩,
+  locally_trivial := λ b, ⟨Z.local_triv_at b, Z.mem_base_set_at b⟩, }
+
+/-- The projection on the base of a topological vector bundle created from core is continuous -/
+lemma continuous_proj : continuous Z.proj :=
+topological_fiber_bundle_core.continuous_proj Z
+
+/-- The projection on the base of a topological vector bundle created from core is an open map -/
+lemma is_open_map_proj : is_open_map Z.proj :=
+topological_fiber_bundle_core.is_open_map_proj Z
 
 end topological_vector_bundle_core