topological_fiber_bundle_core

Stream: new members

[Nicolò Cavalleri]

@Sebastien Gouezel I am playing with your construction topological_fiber_bundle_core and I cannot finish to prove this lemma to be put at the end of topological_fiber_bundle.lean:

section -- to be put somewhere else where there is no `include Z`

@[continuity] lemma _root_.continuous.prod.mk {α : Type*} {β : Type*} [topological_space α]
  [topological_space β] (a : α) : continuous (prod.mk a : β → α × β) :=
continuous_const.prod_mk continuous_id'

end

lemma continuous_sigma_mk (b : B) : @continuous _ _ _ (Z.to_topological_space ι) -- why does it found the sigma topology instead?
  (λ a, (⟨b, a⟩ : (bundle.total_space Z.fiber))) :=
begin
  rw continuous_iff_le_induced,
  unfold topological_fiber_bundle_core.to_topological_space,
  rw induced_generate_from_eq,
  apply le_generate_from,
  simp only [mem_image, exists_prop, mem_Union, mem_singleton_iff], --lemma
  intros s hs,
  rcases hs with ⟨_, ⟨i, t, ht, rfl⟩, rfl⟩,
  simp only [preimage_inter],
  refine is_open.inter _ _,
  {
  sorry,  -- there is not enough API for the generated topology... do I need to write it?
  },
  {
    rw ←preimage_comp,
    simp only [function.comp, local_triv'_apply],
    rw preimage_comp,
    have : continuous (λ (x : Z.fiber b), (Z.coord_change (Z.index_at b) i b) x) :=
    by {
      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),
        simp only [id.def],
        sorry, --this is false, but still it feels like the natural proof...
        })},
    exact (this).is_open_preimage _ ((continuous.prod.mk b).is_open_preimage t ht),
  },
end

can you prove it yourself from scratch / give me some hints / find out why my proof is wrong?