Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-29 17:50 55f32dae

View on Github →

feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545) We construct the pullback bundle of a vector bundle.

Co-authored by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Co-authored by: Floris van Doorn fpvdoorn@gmail.com
Co-authored by: Sebastien Gouezel sebastien.gouezel@univ-rennes1.fr

Estimated changes

Modified src/data/bundle.lean

added def bundle.pullback.lift

added theorem bundle.pullback.lift_mk

added theorem bundle.pullback.proj_lift

added def bundle.pullback

added def bundle.pullback_total_space_embedding

added theorem bundle.pullback_total_space_embedding_snd

modified def bundle.trivial.proj_snd

Modified src/logic/equiv/local_equiv.lean

added theorem local_equiv.eq_symm_apply

Modified src/logic/is_empty.lean

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.eq_symm_apply

Modified src/topology/order.lean

added theorem continuous_empty_function

Modified src/topology/vector_bundle.lean

added theorem inducing_pullback_total_space_embedding

added theorem pullback.continuous_lift

added theorem pullback.continuous_proj

added theorem pullback.continuous_total_space_mk

added def pullback_topology

added theorem topological_vector_bundle.trivialization.open_target

added def topological_vector_bundle.trivialization.pullback