Commit 2022-06-01 17:27 9b3ea03d

View on Github →

feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359) I will wait for a later PR to (maybe) fix the reducibility/simp of these declarations.

Estimated changes

Modified src/data/bundle.lean

deleted def bundle.proj

modified theorem bundle.sigma_mk_eq_total_space_mk

modified theorem bundle.to_total_space_coe

modified theorem bundle.total_space.eta

added def bundle.total_space.proj

modified theorem bundle.total_space.proj_mk

modified def bundle.total_space_mk

Modified src/geometry/manifold/cont_mdiff.lean

Modified src/topology/fiber_bundle.lean

modified theorem topological_fiber_bundle_core.continuous_total_space_mk

modified def topological_fiber_bundle_core.proj

Modified src/topology/vector_bundle.lean

modified theorem topological_vector_bundle.continuous_proj

modified theorem topological_vector_bundle.continuous_total_space_mk

modified theorem topological_vector_bundle.pretrivialization.coe_fst'

modified theorem topological_vector_bundle.pretrivialization.coe_fst

modified theorem topological_vector_bundle.pretrivialization.mem_source

modified theorem topological_vector_bundle.pretrivialization.mk_proj_snd'

modified theorem topological_vector_bundle.pretrivialization.mk_proj_snd

modified theorem topological_vector_bundle.pretrivialization.proj_symm_apply

deleted theorem topological_vector_bundle.pretrivialization.symm_coe_fst'

added theorem topological_vector_bundle.pretrivialization.symm_coe_proj

modified theorem topological_vector_bundle.trivialization.apply_symm_apply'

modified theorem topological_vector_bundle.trivialization.coe_fst'

modified theorem topological_vector_bundle.trivialization.coe_fst

modified theorem topological_vector_bundle.trivialization.mem_source

modified theorem topological_vector_bundle.trivialization.mk_proj_snd'

modified theorem topological_vector_bundle.trivialization.mk_proj_snd

modified theorem topological_vector_bundle.trivialization.prod.continuous_to_fun

modified theorem topological_vector_bundle.trivialization.proj_symm_apply'

deleted theorem topological_vector_bundle.trivialization.symm_coe_fst'

added theorem topological_vector_bundle.trivialization.symm_coe_proj

modified def topological_vector_bundle_core.proj