Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-02 14:35 e473c319

View on Github →

refactor: redefine bundle.total_space (#19221)

  • Use a custom structure for bundle.total_space.
    • Use instead of bundle.total_space_mk.
    • Use bundle.total_space.to_prod instead of equiv.sigma_equiv_prod.
    • Use' (scoped notation) to specify F.
    • Rename bundle.trivial.proj_snd to bundle.total_space.trivial_snd to allow dot notation. Should we just use bundle.total_space.snd since bundle.trivial is now reducible?
  • Add an unused argument to bundle.total_space.
  • Make bundle.trivial and bundle.continuous_linear_map reducible.
  • Drop instances that are no longer needed.

Estimated changes

modified def bundle.zero_section
modified theorem bundle.zero_section_proj
modified theorem bundle.zero_section_snd
modified theorem continuous_on_coord_change
modified theorem trivialization.coe_symmₗ
modified def trivialization.symmL