Patrick Massot (Nov 13 2019 at 21:32):
@Sebastien Gouezel in https://github.com/leanprover-community/mathlib/blob/e2a8e639a0d0f452d162e13c1d5b2804a135c635/src/geometry/manifold/real_instances.lean#L40-L51 I don't understand why there are only half spaces and quadrant. How do you handle intermediate stratas? Say I want a manifold with corners structure on . Which model do you use along edges, away from vertices?
Sebastien Gouezel (Nov 13 2019 at 21:39):
With the quadrant model, you get everything. For instance, if a point
x is away from the boundary, then a small ball around
x looks like a ball in
R^n. If a point
x is on the boundary but not on a corner, then a small ball around
x looks like a ball in the half-space centered at a point on the boundary. And so on: depending on the number
k of zero coordinates of
x, you get a corner of order
Patrick Massot (Nov 14 2019 at 08:00):
Oh I see: you don't ask for anyone to go to the center of the chart. No problem then.
Last updated: May 09 2021 at 09:11 UTC