Session Smooth_Manifolds

Theories

• HOL-Library.Function_Algebras
• HOL-Types_To_Sets.Prerequisites
• HOL-Types_To_Sets.Types_To_Sets
  • File ‹local_typedef.ML›
  • File ‹unoverloading.ML›
  • File ‹internalize_sort.ML›
  • File ‹unoverload_type.ML›
  • File ‹unoverload_def.ML›
• HOL-Types_To_Sets.Group_On_With
• HOL-Types_To_Sets.Linear_Algebra_On_With
• HOL-Types_To_Sets.Linear_Algebra_On
• Analysis_More
• Smooth
• Bump_Function
• Chart
• Topological_Manifold
• Differentiable_Manifold
• Partition_Of_Unity
• Tangent_Space
• Cotangent_Space
• Product_Manifold
• Sphere
• HOL-Library.Quotient_Syntax
• HOL-Library.Quotient_Set
• Projective_Space