Commit 2025-06-19 12:16 46168765

View on Github →

feat: more uses of simps in fiber bundles and vector bundles (#26121)

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

added theorem Bundle.Trivial.toPartialHomeomorph_trivialization_symm_apply

deleted theorem Bundle.Trivial.trivialization_source

added theorem Bundle.Trivial.trivialization_symm_apply

deleted theorem Bundle.Trivial.trivialization_target

deleted theorem Trivialization.baseSet_prod

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

added def Trivialization.Simps.apply

Modified Mathlib/Topology/Homeomorph/Defs.lean

added theorem Equiv.toHomeomorphOfIsInducing_apply

added theorem Equiv.toHomeomorphOfIsInducing_symm_apply

Modified Mathlib/Topology/VectorBundle/Basic.lean

Modified Mathlib/Topology/VectorBundle/Constructions.lean

added theorem Trivialization.prod_apply'

deleted theorem Trivialization.prod_apply