Zulip Chat Archive

Stream: maths

Topic: corners


view this post on Zulip 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 [0,1]3[0, 1]^3. Which model do you use along edges, away from vertices?

view this post on Zulip 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 k.

view this post on Zulip 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