Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-21 14:34 f19dbf29

View on Github →

feat(geometric/manifold): smooth manifolds (#1555)

smooth manifolds
fix docstrings
update docstring
remove out_param

Estimated changes

Created src/geometry/manifold/smooth_manifold_with_corners.lean

added def euclidean_half_space

added def euclidean_space

added theorem model_with_corners.image

added def model_with_corners.prod

added def model_with_corners.tangent

added structure model_with_corners

added def model_with_corners_euclidean_half_space

added theorem model_with_corners_inv_fun_comp

added theorem model_with_corners_left_inv

added theorem model_with_corners_right_inv

added def model_with_corners_self

added theorem model_with_corners_self_local_equiv

added theorem model_with_corners_target

added theorem range_half_space

added def times_cont_diff_groupoid

added theorem times_cont_diff_groupoid_le

added theorem times_cont_diff_groupoid_zero_eq