OAI/Geometry/HyperbolicGroups/SimplexCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite simplex coordinates, with the actual barycentric subspace topology. No CW coordinate comparison is assumed.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.barycentric line 16
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_continuous line 19
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_at line 27
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_off line 30
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_sum line 39
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_mem line 43
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.barycentric_read line 51
  8. def OAI.HyperbolicObstruction.FinitePolyhedron.simplexCoordinates line 61

    Source documentation

    Canonical homeomorphism to a closed simplex with distinct vertices e.

    def simplexCoordinates {e : Fin n → V} (he : Function.Injective e) :
    {weights : Fin n → ℝ // (∀ index, 0 ≤ weights index) ∧ ∑ index, weights index = 1} ≃ₜ
      simplex (Finset.univ.image e) where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.simplex

  9. def OAI.HyperbolicObstruction.FinitePolyhedron.closedSimplexHomeomorph line 78

    Source documentation

    The closed simplex in the carrier and its ambient barycentric subtype carry exactly the same topology.

    def closedSimplexHomeomorph {s : Finset V} (hs : s ∈ K.faces) :
    simplex s ≃ₜ {x : Carrier K // x.val ∈ simplex s} where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.simplex, OAI.HyperbolicObstruction.FinitePolyhedron.Carrier