Mathlib v3 is deprecated. Go to Mathlib v4

Def bundle.pullback

Modification history

2023-07-02 14:35

src/data/bundle.lean

refactor: redefine `bundle.total_space` (#19221) …

Modified bundle.pullback View on Github →

2022-07-30 06:36

src/data/bundle.lean

refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542) …

Modified bundle.pullback View on Github →

2022-05-29 17:50

src/data/bundle.lean

feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545) …

Added bundle.pullback View on Github →