mathlib
dd9a0ea2 - feat(geometry/manifold): add `charted_space` and `model_with_corners` for pi types (#6578)

Commit

4 years ago

feat(geometry/manifold): add `charted_space` and `model_with_corners` for pi types (#6578) Also use `set.image2` in the `charted_space` instance for `model_prod`.

Author

urkud

Parents

7bed785b

mathlib dd9a0ea2 - feat(geometry/manifold): add `charted_space` and `model_with_corners` for pi types (#6578)

mathlib
dd9a0ea2 - feat(geometry/manifold): add `charted_space` and `model_with_corners` for pi types (#6578)