# Zulip Chat Archive

## Stream: maths

### Topic: corners

#### 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$. 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 `k`

.

#### 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