diff --git a/src/topology/fiber_bundle.lean b/src/topology/fiber_bundle.lean
index e681c9ab9cfe3..e1ac336331a14 100644
--- a/src/topology/fiber_bundle.lean
+++ b/src/topology/fiber_bundle.lean
@@ -1087,76 +1087,80 @@ topology in such a way that there is a fiber bundle structure for which the loca
 are also local homeomorphism and hence local trivializations. -/
 @[nolint has_inhabited_instance]
 structure topological_fiber_prebundle (proj : Z → B) :=
+(pretrivialization_atlas : set (pretrivialization F proj))
 (pretrivialization_at : B → pretrivialization F proj)
 (mem_base_pretrivialization_at : ∀ x : B, x ∈ (pretrivialization_at x).base_set)
-(continuous_triv_change : ∀ x y : B, continuous_on ((pretrivialization_at x) ∘
-  (pretrivialization_at y).to_local_equiv.symm) ((pretrivialization_at y).target ∩
-  ((pretrivialization_at y).to_local_equiv.symm ⁻¹' (pretrivialization_at x).source)))
+(pretrivialization_mem_atlas : ∀ x : B, pretrivialization_at x ∈ pretrivialization_atlas)
+(continuous_triv_change : ∀ e e' ∈ pretrivialization_atlas,
+  continuous_on (e ∘ e'.to_local_equiv.symm) (e'.target ∩ (e'.to_local_equiv.symm ⁻¹' e.source)))
 
 namespace topological_fiber_prebundle
 
-variables {F} (a : topological_fiber_prebundle F proj) (x : B)
+variables {F} (a : topological_fiber_prebundle F proj) {e : pretrivialization F proj}
 
 /-- Topology on the total space that will make the prebundle into a bundle. -/
 def total_space_topology (a : topological_fiber_prebundle F proj) : topological_space Z :=
-⨆ x : B, coinduced (a.pretrivialization_at x).set_symm (subtype.topological_space)
+⨆ (e : pretrivialization F proj) (he : e ∈ a.pretrivialization_atlas),
+  coinduced e.set_symm (subtype.topological_space)
 
-lemma continuous_symm_pretrivialization_at : @continuous_on _ _ _ a.total_space_topology
-  (a.pretrivialization_at x).to_local_equiv.symm (a.pretrivialization_at x).target :=
+lemma continuous_symm_of_mem_pretrivialization_atlas (he : e ∈ a.pretrivialization_atlas) :
+  @continuous_on _ _ _ a.total_space_topology
+  e.to_local_equiv.symm e.target :=
 begin
   refine id (λ z H, id (λ U h, preimage_nhds_within_coinduced' H
-    (a.pretrivialization_at x).open_target (le_def.1 (nhds_mono _) U h))),
-  exact le_supr _ x,
+    e.open_target (le_def.1 (nhds_mono _) U h))),
+  exact le_bsupr e he,
 end
 
-lemma is_open_source_pretrivialization_at :
-  @is_open _ a.total_space_topology (a.pretrivialization_at x).source :=
+lemma is_open_source (e : pretrivialization F proj) : @is_open _ a.total_space_topology e.source :=
 begin
   letI := a.total_space_topology,
-  refine is_open_supr_iff.mpr (λ y, is_open_coinduced.mpr (is_open_induced_iff.mpr
-    ⟨(a.pretrivialization_at x).target, (a.pretrivialization_at x).open_target, _⟩)),
-  rw [pretrivialization.set_symm, restrict, (a.pretrivialization_at x).target_eq,
-    (a.pretrivialization_at x).source_eq, preimage_comp, subtype.preimage_coe_eq_preimage_coe_iff,
-    (a.pretrivialization_at y).target_eq, prod_inter_prod, inter_univ,
+  refine is_open_supr_iff.mpr (λ e', _),
+  refine is_open_supr_iff.mpr (λ he', _),
+  refine is_open_coinduced.mpr (is_open_induced_iff.mpr ⟨e.target, e.open_target, _⟩),
+  rw [pretrivialization.set_symm, restrict, e.target_eq,
+    e.source_eq, preimage_comp, subtype.preimage_coe_eq_preimage_coe_iff,
+    e'.target_eq, prod_inter_prod, inter_univ,
     pretrivialization.preimage_symm_proj_inter],
 end
 
-lemma is_open_target_pretrivialization_at_inter (x y : B) :
-  is_open ((a.pretrivialization_at y).to_local_equiv.target ∩
-  (a.pretrivialization_at y).to_local_equiv.symm ⁻¹' (a.pretrivialization_at x).source) :=
+lemma is_open_target_of_mem_pretrivialization_atlas_inter (e e' : pretrivialization F proj)
+  (he' : e' ∈ a.pretrivialization_atlas) :
+  is_open (e'.to_local_equiv.target ∩ e'.to_local_equiv.symm ⁻¹' e.source) :=
 begin
   letI := a.total_space_topology,
-  obtain ⟨u, hu1, hu2⟩ := continuous_on_iff'.mp (a.continuous_symm_pretrivialization_at y)
-    (a.pretrivialization_at x).source (a.is_open_source_pretrivialization_at x),
+  obtain ⟨u, hu1, hu2⟩ := continuous_on_iff'.mp (a.continuous_symm_of_mem_pretrivialization_atlas
+    he') e.source (a.is_open_source e),
   rw [inter_comm, hu2],
-  exact hu1.inter (a.pretrivialization_at y).open_target,
+  exact hu1.inter e'.open_target,
 end
 
 /-- Promotion from a `pretrivialization` to a `trivialization`. -/
-def trivialization_at (a : topological_fiber_prebundle F proj) (x : B) :
+def trivialization_of_mem_pretrivialization_atlas (he : e ∈ a.pretrivialization_atlas) :
   @trivialization B F Z _ _ a.total_space_topology proj :=
-{ open_source := a.is_open_source_pretrivialization_at x,
+{ open_source := a.is_open_source e,
   continuous_to_fun := begin
     letI := a.total_space_topology,
-    refine continuous_on_iff'.mpr (λ s hs, ⟨(a.pretrivialization_at x) ⁻¹' s ∩
-      (a.pretrivialization_at x).source, (is_open_supr_iff.mpr (λ y, _)),
+    refine continuous_on_iff'.mpr (λ s hs, ⟨e ⁻¹' s ∩ e.source, (is_open_supr_iff.mpr (λ e', _)),
       by { rw [inter_assoc, inter_self], refl }⟩),
+    refine (is_open_supr_iff.mpr (λ he', _)),
     rw [is_open_coinduced, is_open_induced_iff],
-    obtain ⟨u, hu1, hu2⟩ := continuous_on_iff'.mp (a.continuous_triv_change x y) s hs,
-    have hu3 := congr_arg (λ s, (λ x : (a.pretrivialization_at y).target, (x : B × F)) ⁻¹' s) hu2,
+    obtain ⟨u, hu1, hu2⟩ := continuous_on_iff'.mp (a.continuous_triv_change _ he _ he') s hs,
+    have hu3 := congr_arg (λ s, (λ x : e'.target, (x : B × F)) ⁻¹' s) hu2,
     simp only [subtype.coe_preimage_self, preimage_inter, univ_inter] at hu3,
-    refine ⟨u ∩ (a.pretrivialization_at y).to_local_equiv.target ∩
-      ((a.pretrivialization_at y).to_local_equiv.symm ⁻¹' (a.pretrivialization_at x).source), _, by
+    refine ⟨u ∩ e'.to_local_equiv.target ∩
+      (e'.to_local_equiv.symm ⁻¹' e.source), _, by
       { simp only [preimage_inter, inter_univ, subtype.coe_preimage_self, hu3.symm], refl }⟩,
     rw inter_assoc,
-    exact hu1.inter (a.is_open_target_pretrivialization_at_inter x y),
+    exact hu1.inter (a.is_open_target_of_mem_pretrivialization_atlas_inter e e' he'),
   end,
-  continuous_inv_fun := a.continuous_symm_pretrivialization_at x,
-  ..(a.pretrivialization_at x) }
+  continuous_inv_fun := a.continuous_symm_of_mem_pretrivialization_atlas he,
+  .. e }
 
 lemma is_topological_fiber_bundle :
   @is_topological_fiber_bundle B F Z _ _ a.total_space_topology proj :=
-λ x, ⟨a.trivialization_at x, a.mem_base_pretrivialization_at x ⟩
+λ x, ⟨a.trivialization_of_mem_pretrivialization_atlas (a.pretrivialization_mem_atlas x),
+  a.mem_base_pretrivialization_at x ⟩
 
 lemma continuous_proj : @continuous _ _ a.total_space_topology _ proj :=
 by { letI := a.total_space_topology, exact a.is_topological_fiber_bundle.continuous_proj, }
diff --git a/src/topology/vector_bundle.lean b/src/topology/vector_bundle.lean
index 4a975fe5e1f54..079a1c1c29ae0 100644
--- a/src/topology/vector_bundle.lean
+++ b/src/topology/vector_bundle.lean
@@ -18,27 +18,23 @@ Let `B` be the base space. In our formalism, a topological vector bundle is by d
 `Σ (x : B), E x`, with the interest that one can put another topology than on `Σ (x : B), E x`
 which has the disjoint union topology.
 
-To have a topological vector bundle structure on `bundle.total_space E`,
-one should addtionally have the following data:
+To have a topological vector bundle structure on `bundle.total_space E`, one should
+additionally have the following data:
 
 * `F` should be a topological space and a module over a semiring `R`;
 * There should be a topology on `bundle.total_space E`, for which the projection to `B` is
 a topological fiber bundle with fiber `F` (in particular, each fiber `E x` is homeomorphic to `F`);
 * For each `x`, the fiber `E x` should be a topological vector space over `R`, and the injection
 from `E x` to `bundle.total_space F E` should be an embedding;
-* The most important condition: around each point, there should be a bundle trivialization which
-is a continuous linear equiv in the fibers.
-
-If all these conditions are satisfied, we register the typeclass
-`topological_vector_bundle R F E`. We emphasize that the data is provided by other classes, and
-that the `topological_vector_bundle` class is `Prop`-valued.
-
-The point of this formalism is that it is unbundled in the sense that the total space of the bundle
-is a type with a topology, with which one can work or put further structure, and still one can
-perform operations on topological vector bundles.  For instance, assume that `E₁ : B → Type*` and
-`E₂ : B → Type*` define two topological vector bundles over `R` with fiber models `F₁` and `F₂`
-which are normed spaces. Then we construct the vector bundle `E₁ ×ᵇ E₂` of direct sums, with fiber
-`E x := (E₁ x × E₂ x)`. Then one can endow `bundle.total_space (E₁ ×ᵇ E₂)` with a topological vector
+* There should be a distinguished set of bundle trivializations (which are continuous linear equivs
+in the fibres), the "trivialization atlas"
+* There should be a choice of bundle trivialization at each point, which belongs to this atlas.
+
+If all these conditions are satisfied, we register the typeclass `topological_vector_bundle R F E`.
+
+If `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `R` with fiber
+models `F₁` and `F₂`, denote by `E₁ ×ᵇ E₂` the sigma type of direct sums, with fiber
+`E x := (E₁ x × E₂ x)`. We can endow `bundle.total_space (E₁ ×ᵇ E₂)` with a topological vector
 bundle structure, `bundle.prod.topological_vector_bundle`.
 
 A similar construction (which is yet to be formalized) can be done for the vector bundle of
@@ -49,6 +45,16 @@ topology on continuous linear maps between general topological vector spaces).
 products of topological vector bundles, exterior algebras, and so on, where the topology can be
 defined using a norm on the fiber model if this helps.
 
+## TODO
+
+The definition `topological_vector_bundle` is currently not the standard definition given in the
+literature, but rather a variant definition which agrees *in finite dimension* with the standard
+definition.  The standard definition in the literature requires a further condition on the
+compatibility of transition functions, see
+https://mathoverflow.net/questions/4943/vector-bundle-with-non-smoothly-varying-transition-functions/4997#4997
+https://mathoverflow.net/questions/54550/the-third-axiom-in-the-definition-of-infinite-dimensional-vector-bundles-why/54706#54706
+This will be fixed in a future refactor.
+
 ## Tags
 Vector bundle
 -/
@@ -116,23 +122,20 @@ variables [∀ x, topological_space (E x)]
 space) has a topological vector space structure with fiber `F` (denoted with
 `topological_vector_bundle R F E`) if around every point there is a fiber bundle trivialization
 which is linear in the fibers. -/
-class topological_vector_bundle : Prop :=
+class topological_vector_bundle :=
 (total_space_mk_inducing [] : ∀ (b : B), inducing (total_space_mk E b))
-(locally_trivial [] : ∀ b : B, ∃ e : topological_vector_bundle.trivialization R F E, b ∈ e.base_set)
+(trivialization_atlas [] : set (trivialization R F E))
+(trivialization_at [] : B → trivialization R F E)
+(mem_base_set_trivialization_at [] : ∀ b : B, b ∈ (trivialization_at b).base_set)
+(trivialization_mem_atlas [] : ∀ b : B, trivialization_at b ∈ trivialization_atlas)
+
+export topological_vector_bundle (trivialization_atlas trivialization_at
+  mem_base_set_trivialization_at trivialization_mem_atlas)
 
 variable [topological_vector_bundle R F E]
 
 namespace topological_vector_bundle
 
-/-- `trivialization_at R F E b` is some choice of trivialization of a vector bundle whose base set
-contains a given point `b`. -/
-def trivialization_at : Π b : B, trivialization R F E :=
-λ b, classical.some (locally_trivial R F E b)
-
-@[simp, mfld_simps] lemma mem_base_set_trivialization_at (b : B) :
-  b ∈ (trivialization_at R F E b).base_set :=
-classical.some_spec (locally_trivial R F E b)
-
 @[simp, mfld_simps] lemma mem_source_trivialization_at (z : total_space E) :
   z ∈ (trivialization_at R F E z.1).source :=
 by { rw topological_fiber_bundle.trivialization.mem_source, apply mem_base_set_trivialization_at }
@@ -278,7 +281,10 @@ def trivial_topological_vector_bundle.trivialization : trivialization R F (bundl
 
 instance trivial_bundle.topological_vector_bundle :
   topological_vector_bundle R F (bundle.trivial B F) :=
-{ locally_trivial := λ x, ⟨trivial_topological_vector_bundle.trivialization R B F, mem_univ x⟩,
+{ trivialization_atlas := {trivial_topological_vector_bundle.trivialization R B F},
+  trivialization_at := λ x, trivial_topological_vector_bundle.trivialization R B F,
+  mem_base_set_trivialization_at := mem_univ,
+  trivialization_mem_atlas := λ x, mem_singleton _,
   total_space_mk_inducing := λ b, ⟨begin
     have : (λ (x : trivial B F b), x) = @id F, by { ext x, refl },
     simp only [total_space.topological_space, induced_inf, induced_compose, function.comp, proj,
@@ -409,7 +415,7 @@ topological_fiber_bundle_core.to_topological_space ι ↑Z
 
 variables {ι} (b : B) (a : F)
 
-@[simp, mfld_simps] lemma coe_cord_change (i j : ι) :
+@[simp, mfld_simps] lemma coe_coord_change (i j : ι) :
   topological_fiber_bundle_core.coord_change ↑Z i j b = Z.coord_change i j b := rfl
 
 /-- Extended version of the local trivialization of a fiber bundle constructed from core,
@@ -471,7 +477,10 @@ instance : topological_vector_bundle R F Z.fiber :=
         exact ha.2.2, },
       { simp only [mem_prod, mem_preimage, mem_inter_eq, 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⟩, }
+  trivialization_atlas := set.range Z.local_triv,
+  trivialization_at := Z.local_triv_at,
+  mem_base_set_trivialization_at := Z.mem_base_set_at,
+  trivialization_mem_atlas := λ b, ⟨Z.index_at b, rfl⟩ }
 
 /-- The projection on the base of a topological vector bundle created from core is continuous -/
 @[continuity] lemma continuous_proj : continuous Z.proj :=
@@ -496,14 +505,15 @@ open topological_space
 /-- This structure permits to define a vector bundle when trivializations are given as local
 equivalences but there is not yet a topology on the total space. The total space is hence given a
 topology in such a way that there is a fiber bundle structure for which the local equivalences
-are also local homeomorphism and hence vector bundle trivializations. -/
+are also local homeomorphisms and hence vector bundle trivializations. -/
 @[nolint has_inhabited_instance]
 structure topological_vector_prebundle :=
+(pretrivialization_atlas : set (topological_vector_bundle.pretrivialization R F E))
 (pretrivialization_at : B → topological_vector_bundle.pretrivialization R F E)
 (mem_base_pretrivialization_at : ∀ x : B, x ∈ (pretrivialization_at x).base_set)
-(continuous_triv_change : ∀ x y : B, continuous_on ((pretrivialization_at x) ∘
-  (pretrivialization_at y).to_local_equiv.symm) ((pretrivialization_at y).target ∩
-  ((pretrivialization_at y).to_local_equiv.symm ⁻¹' (pretrivialization_at x).source)))
+(pretrivialization_mem_atlas : ∀ x : B, pretrivialization_at x ∈ pretrivialization_atlas)
+(continuous_triv_change : ∀ e e' ∈ pretrivialization_atlas,
+  continuous_on (e ∘ e'.to_local_equiv.symm) (e'.target ∩ (e'.to_local_equiv.symm ⁻¹' e.source)))
 (total_space_mk_inducing : ∀ (b : B), inducing ((pretrivialization_at b) ∘ (total_space_mk E b)))
 
 namespace topological_vector_prebundle
@@ -513,7 +523,15 @@ variables {R E F}
 /-- Natural identification of `topological_vector_prebundle` as a `topological_fiber_prebundle`. -/
 def to_topological_fiber_prebundle (a : topological_vector_prebundle R F E) :
   topological_fiber_prebundle F (proj E) :=
-{ pretrivialization_at := λ x, a.pretrivialization_at x, ..a }
+{ pretrivialization_atlas :=
+    pretrivialization.to_fiber_bundle_pretrivialization '' a.pretrivialization_atlas,
+  pretrivialization_at := λ x, (a.pretrivialization_at x).to_fiber_bundle_pretrivialization,
+  pretrivialization_mem_atlas := λ x, ⟨_, a.pretrivialization_mem_atlas x, rfl⟩,
+  continuous_triv_change := begin
+    rintros _ ⟨e, he, rfl⟩ _ ⟨e', he', rfl⟩,
+    exact a.continuous_triv_change _ he _ he',
+  end,
+  .. a }
 
 /-- Topology on the total space that will make the prebundle into a bundle. -/
 def total_space_topology (a : topological_vector_prebundle R F E) :
@@ -522,12 +540,13 @@ a.to_topological_fiber_prebundle.total_space_topology
 
 /-- Promotion from a `topologial_vector_prebundle.trivialization` to a
   `topological_vector_bundle.trivialization`. -/
-def trivialization_at (a : topological_vector_prebundle R F E) (x : B) :
+def trivialization_of_mem_pretrivialization_atlas (a : topological_vector_prebundle R F E)
+  {e : topological_vector_bundle.pretrivialization R F E} (he : e ∈ a.pretrivialization_atlas) :
   @topological_vector_bundle.trivialization R _ F E _ _ _ _ _ _ _ a.total_space_topology :=
 begin
   letI := a.total_space_topology,
-  exact { linear := (a.pretrivialization_at x).linear,
-  ..a.to_topological_fiber_prebundle.trivialization_at x }
+  exact { linear := e.linear,
+  ..a.to_topological_fiber_prebundle.trivialization_of_mem_pretrivialization_atlas ⟨e, he, rfl⟩ }
 end
 
 variable (a : topological_vector_prebundle R F E)
@@ -553,28 +572,41 @@ end
   @continuous _ _ _ a.total_space_topology (total_space_mk E b) :=
 begin
   letI := a.total_space_topology,
-  rw (a.trivialization_at b).to_local_homeomorph.continuous_iff_continuous_comp_left
+  let e := a.trivialization_of_mem_pretrivialization_atlas (a.pretrivialization_mem_atlas b),
+  rw e.to_local_homeomorph.continuous_iff_continuous_comp_left
     (a.total_space_mk_preimage_source b),
   exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.total_space_mk_inducing b).induced).1,
 end
 
 lemma inducing_total_space_mk_of_inducing_comp (b : B)
-  (h : inducing ((a.trivialization_at b) ∘ (total_space_mk E b))) :
+  (h : inducing ((a.pretrivialization_at b) ∘ (total_space_mk E b))) :
   @inducing _ _ _ a.total_space_topology (total_space_mk E b) :=
 begin
   letI := a.total_space_topology,
   rw ←restrict_comp_cod_restrict (a.mem_trivialization_at_source b) at h,
   apply inducing.of_cod_restrict (a.mem_trivialization_at_source b),
   refine inducing_of_inducing_compose _ (continuous_on_iff_continuous_restrict.mp
-    (a.trivialization_at b).continuous_to_fun) h,
+    (a.trivialization_of_mem_pretrivialization_atlas
+    (a.pretrivialization_mem_atlas b)).continuous_to_fun) h,
   exact (a.continuous_total_space_mk b).cod_restrict (a.mem_trivialization_at_source b),
 end
 
-lemma to_topological_vector_bundle :
+/-- Make a `topological_vector_bundle` from a `topological_vector_prebundle`.  Concretely this means
+that, given a `topological_vector_prebundle` structure for a sigma-type `E` -- which consists of a
+number of "pretrivializations" identifying parts of `E` with product spaces `U × F` -- one
+establishes that for the topology constructed on the sigma-type using
+`topological_vector_prebundle.total_space_topology`, these "pretrivializations" are actually
+"trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
+def to_topological_vector_bundle :
   @topological_vector_bundle R _ F E _ _ _ _ _ _ _ a.total_space_topology _ :=
 { total_space_mk_inducing := λ b, a.inducing_total_space_mk_of_inducing_comp b
     (a.total_space_mk_inducing b),
-  locally_trivial := λ b, ⟨a.trivialization_at b, a.mem_base_pretrivialization_at b⟩ }
+  trivialization_atlas := {e | ∃ e₀ (he₀ : e₀ ∈ a.pretrivialization_atlas),
+    e = a.trivialization_of_mem_pretrivialization_atlas he₀},
+  trivialization_at := λ x, a.trivialization_of_mem_pretrivialization_atlas
+    (a.pretrivialization_mem_atlas x),
+  mem_base_set_trivialization_at := a.mem_base_pretrivialization_at,
+  trivialization_mem_atlas := λ x, ⟨_, a.pretrivialization_mem_atlas x, rfl⟩ }
 
 end topological_vector_prebundle
 
@@ -778,12 +810,13 @@ instance _root_.bundle.prod.topological_vector_bundle :
     rw (prod.inducing_diag E₁ E₂).inducing_iff,
     exact (total_space_mk_inducing R F₁ E₁ b).prod_mk (total_space_mk_inducing R F₂ E₂ b),
   end,
-  locally_trivial := λ b,
-  begin
-    obtain ⟨e₁, he₁⟩ := locally_trivial R F₁ E₁ b,
-    obtain ⟨e₂, he₂⟩ := locally_trivial R F₂ E₂ b,
-    exact ⟨e₁.prod e₂, he₁, he₂⟩
-  end }
+  trivialization_atlas := (λ (p : trivialization R F₁ E₁ × trivialization R F₂ E₂), p.1.prod p.2) ''
+    (trivialization_atlas R F₁ E₁ ×ˢ trivialization_atlas R F₂ E₂),
+  trivialization_at := λ b, (trivialization_at R F₁ E₁ b).prod (trivialization_at R F₂ E₂ b),
+  mem_base_set_trivialization_at :=
+    λ b, ⟨mem_base_set_trivialization_at R F₁ E₁ b, mem_base_set_trivialization_at R F₂ E₂ b⟩,
+  trivialization_mem_atlas := λ b,
+    ⟨(_, _), ⟨trivialization_mem_atlas R F₁ E₁ b, trivialization_mem_atlas R F₂ E₂ b⟩, rfl⟩ }
 
 variables {R F₁ E₁ F₂ E₂}