Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-27 22:59 708faa9f

View on Github →

feat(geometry/manifold/manifold): define manifolds (#1422)

feat(geometry/manifold/manifold): define manifolds
Update src/geometry/manifold/manifold.lean Typo Co-Authored-By: Johan Commelin johan@commelin.net
reviewer comments
notations, comments
Update src/geometry/manifold/manifold.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/geometry/manifold/manifold.lean Co-Authored-By: Scott Morrison scott@tqft.net
manifolds: reviewers comments
comment on notation for composition
add documentation on atlases and structomorphisms

Estimated changes

Created src/geometry/manifold/manifold.lean

added theorem chart_at_model_space_eq

added def continuous_groupoid

added def groupoid_of_pregroupoid

added theorem groupoid_of_pregroupoid_le

added theorem has_groupoid_of_le

added def id_groupoid

added def manifold_core.local_homeomorph

added theorem manifold_core.open_source'

added theorem manifold_core.open_target

added def manifold_core.to_manifold

added structure manifold_core

added theorem mem_groupoid_of_pregroupoid

added theorem model_space_atlas

added structure pregroupoid

added def structomorph.refl

added def structomorph.symm

added def structomorph.trans

added structure structomorph

added structure structure_groupoid