Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-15 15:46 6a4d298c

View on Github →

chore(topology/vector_bundle): generalize to topological semimodules (#7183)

Estimated changes

Modified src/topology/vector_bundle.lean

modified def topological_vector_bundle.trivial_bundle_trivialization

modified def topological_vector_bundle.trivialization.continuous_linear_equiv_at

modified theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply'

modified theorem topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply

modified theorem topological_vector_bundle.trivialization.mem_source

modified def topological_vector_bundle.trivialization_at