Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 14:09 15e8bc48

View on Github →

feat(topology/vector_bundle): define pretrivialization.symm (#14192)

Also adds some other useful lemmas about (pre)trivializations
This splits out the part of #8545 that is unrelated to pullbacks

Co-authored by Nicolo Cavalleri nico@cavalleri.net

Estimated changes

Modified src/data/bundle.lean

added theorem bundle.coe_snd

added theorem bundle.sigma_mk_eq_total_space_mk

modified theorem bundle.to_total_space_coe

added theorem bundle.total_space.eta

added theorem bundle.total_space.mk_cast

added theorem bundle.total_space.proj_mk

Modified src/topology/fiber_bundle.lean

Modified src/topology/vector_bundle.lean

added theorem topological_vector_bundle.continuous_total_space_mk

added theorem topological_vector_bundle.pretrivialization.apply_mk_symm

added theorem topological_vector_bundle.pretrivialization.apply_symm_apply'

added theorem topological_vector_bundle.pretrivialization.apply_symm_apply

added theorem topological_vector_bundle.pretrivialization.coe_coe

added theorem topological_vector_bundle.pretrivialization.coe_coe_fst

added theorem topological_vector_bundle.pretrivialization.coe_fst'

added theorem topological_vector_bundle.pretrivialization.coe_fst

added theorem topological_vector_bundle.pretrivialization.coe_mem_source

added theorem topological_vector_bundle.pretrivialization.linear

added def topological_vector_bundle.pretrivialization.linear_equiv_at

added theorem topological_vector_bundle.pretrivialization.mem_source

added theorem topological_vector_bundle.pretrivialization.mem_target

added theorem topological_vector_bundle.pretrivialization.mk_mem_target

added theorem topological_vector_bundle.pretrivialization.mk_proj_snd'

added theorem topological_vector_bundle.pretrivialization.mk_proj_snd

added theorem topological_vector_bundle.pretrivialization.mk_symm

added theorem topological_vector_bundle.pretrivialization.preimage_symm_proj_base_set

added theorem topological_vector_bundle.pretrivialization.proj_symm_apply'

added theorem topological_vector_bundle.pretrivialization.proj_symm_apply

added theorem topological_vector_bundle.pretrivialization.symm_apply

added theorem topological_vector_bundle.pretrivialization.symm_apply_apply

added theorem topological_vector_bundle.pretrivialization.symm_apply_apply_mk

added theorem topological_vector_bundle.pretrivialization.symm_apply_mk_proj

added theorem topological_vector_bundle.pretrivialization.symm_apply_of_not_mem

added theorem topological_vector_bundle.pretrivialization.symm_coe_fst'

added theorem topological_vector_bundle.pretrivialization.symm_proj_apply

added theorem topological_vector_bundle.trivialization.apply_mk_symm

added theorem topological_vector_bundle.trivialization.apply_symm_apply'

added theorem topological_vector_bundle.trivialization.apply_symm_apply

modified theorem topological_vector_bundle.trivialization.coe_coe

added theorem topological_vector_bundle.trivialization.coe_coe_fst

added theorem topological_vector_bundle.trivialization.coe_fst'

modified theorem topological_vector_bundle.trivialization.coe_fst

added theorem topological_vector_bundle.trivialization.coe_mem_source

added theorem topological_vector_bundle.trivialization.continuous_on_symm

added theorem topological_vector_bundle.trivialization.map_target

modified theorem topological_vector_bundle.trivialization.mem_source

added theorem topological_vector_bundle.trivialization.mem_target

added theorem topological_vector_bundle.trivialization.mk_mem_target

added theorem topological_vector_bundle.trivialization.mk_proj_snd'

added theorem topological_vector_bundle.trivialization.mk_proj_snd

added theorem topological_vector_bundle.trivialization.mk_symm

added theorem topological_vector_bundle.trivialization.proj_symm_apply'

added theorem topological_vector_bundle.trivialization.proj_symm_apply

added theorem topological_vector_bundle.trivialization.source_inter_preimage_target_inter

added theorem topological_vector_bundle.trivialization.symm_apply

added theorem topological_vector_bundle.trivialization.symm_apply_apply

added theorem topological_vector_bundle.trivialization.symm_apply_apply_mk

added theorem topological_vector_bundle.trivialization.symm_apply_of_not_mem

added theorem topological_vector_bundle.trivialization.symm_coe_fst'

added theorem topological_vector_bundle.trivialization.symm_proj_apply

modified def topological_vector_bundle.trivialization.to_pretrivialization