Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 09:11 9ff42fdd

View on Github →

feat(topology/fiber_bundle): lemmas about e.symm.trans e' (#13168)

Estimated changes

Modified src/topology/fiber_bundle.lean

added theorem topological_fiber_bundle.pretrivialization.symm_trans_source_eq

added theorem topological_fiber_bundle.pretrivialization.symm_trans_symm

added theorem topological_fiber_bundle.pretrivialization.symm_trans_target_eq

added theorem topological_fiber_bundle.trivialization.symm_trans_source_eq

added theorem topological_fiber_bundle.trivialization.symm_trans_target_eq