ClosedCoverGluing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Literal continuous gluing on locally finite closed covers. This is used for cell-by-cell homotopies; it does not assume cell extensions exist.

def OAI.HyperbolicObstruction.ClosedCoverGluing.glue line 20
Source documentation
Gluing is with the actual source topology, not a replacement quotient.
```
def glue : C(X,Y) where
…
```
lemma OAI.HyperbolicObstruction.ClosedCoverGluing.glue_apply line 32
lemma OAI.HyperbolicObstruction.ClosedCoverGluing.glue_eq line 37
def OAI.HyperbolicObstruction.ClosedCoverGluing.gluePrism line 43
Source documentation
A homotopy prescribed continuously on each closed cell glues once the literal formulas coincide on intersections.
```
def gluePrism (H : ∀ j, C(I × S j,Y))
    (ha : ∀ i j (t : I) x (hi : x ∈ S i) (hj : x ∈ S j),
      H i (t,⟨x,hi⟩) = H j (t,⟨x,hj⟩)) : C(I × X,Y) := by
…
```
lemma OAI.HyperbolicObstruction.ClosedCoverGluing.gluePrism_apply line 60