Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 11:29 3d6c3b6d

View on Github →

feat(geometry/manifold|topology): add simps and ext attributes (#15314)

From the sphere eversion project

Estimated changes

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

modified def model_with_corners.prod

added def model_with_corners.simps.apply

added def model_with_corners.simps.symm_apply

Modified src/geometry/manifold/tangent_bundle.lean

modified def tangent_bundle_core

Modified src/topology/fiber_bundle.lean

added theorem topological_fiber_bundle.trivialization.to_pretrivialization_injective

Modified src/topology/vector_bundle/basic.lean

added theorem topological_vector_bundle.trivialization.to_pretrivialization_injective