OAI/Analysis/SphereIsometry/BarycentricZero.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The zero-dimensional subdivision and its empty codimension-one face

The subdivision of a zero-dimensional complex has one vertex for each old singleton face. In particular, iterated subdivision of the point has one top face, incident to its unique empty codimension-one face.

  1. theorem OAI.Tingley.FiniteComplex.incidentTop_empty line 22
  2. theorem OAI.Tingley.FiniteComplex.sd_topCells_zero_card line 28
  3. theorem OAI.Tingley.FiniteComplex.sd_pure_zero line 62
  4. theorem OAI.Tingley.iter_topCells_zero_card line 81
  5. theorem OAI.Tingley.iter_incidentTop_zero_card line 107