corners

Stream: maths

[Patrick Massot]

@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 $[0, 1]^3$. Which model do you use along edges, away from vertices?

[Sebastien Gouezel]

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 k.

[Patrick Massot]

Oh I see: you don't ask for anyone to go to the center of the chart. No problem then.