OAI/Combinatorics/CompleteCrossing/Subdivision.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Affine polygonal subdivisions and chain parametrizations.

  1. structure OAI.Paper170.AffineCoverData line 17

    Source documentation

    An affine cover retaining its actual interval endpoints.

    structure AffineCoverData {a b : Plane} (γ : Path a b) where
…

    Mentions: OAI.Paper170.Plane

  2. def OAI.Paper170.AffineCoverData.segment line 24
  3. def OAI.Paper170.AffineCoverData.trans line 39
  4. lemma OAI.Paper170.AffineCoverData.trans_endpoints line 85
  5. lemma OAI.Paper170.AffineCoverData.subdivision line 97
  6. lemma OAI.Paper170.polygonalArcPath_safe_cover line 168
  7. def OAI.Paper170.PolygonalParametrization.cast line 195
  8. lemma OAI.Paper170.chain_subdivision_avoiding line 206