PathLocalToGlobal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite-partition local-to-global principle for homotopy classes of actual continuous paths. This will convert open-star control into edge generation.

abbrev OAI.HyperbolicObstruction.PathLocalToGlobal.Q line 13
lemma OAI.HyperbolicObstruction.PathLocalToGlobal.cast line 16

theorem OAI.HyperbolicObstruction.PathLocalToGlobal.of_open_cover line 22

Source documentation

No subdivision or simplicial approximation assumption is made: the partition is obtained from compactness of the actual unit interval.

theorem of_open_cover {ι : Type*} (U : ι → Set X)
    (hU : ∀ i, IsOpen (U i)) (cover : ∀ x, ∃ i, x ∈ U i)
    (hrefl : ∀ x, R x x (.refl x))
    (htrans : ∀ {x y z} {p : Q x y} {q : Q y z}, R x y p → R y z q → R x z (p.trans q))
    (hlocal : ∀ i {x y} (p : Path x y), (∀ t, p t ∈ U i) → R x y (.mk p))
    {x y : X} (p : Path x y) : R x y (.mk p) := by
…

Mentions: OAI.HyperbolicObstruction.PathLocalToGlobal.Q