Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-17 14:48 d8dc1445

View on Github →

feat(geometry/manifold): smooth bundles, tangent bundle (#1607)

  • feat(geometry/manifold): smooth bundles, tangent bundle
  • remove decidable in preamble
  • Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • comments
  • cleanup
  • oops, forgot squeeze_simp
  • simpa instead of simp
  • oops
  • much better docstrings
  • improved formatting
  • space after forall
  • fix build
  • fix build, continuous.smul
  • minor improvements

Estimated changes

added structure basic_smooth_bundle_core
added def tangent_bundle
added def tangent_space
added theorem continuous.smul
deleted theorem continuous_smul'
modified theorem continuous_smul