CoverBoundary.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.group_prefix_rotate line 17
Source documentation
Prefix coordinates really close at the last side. This uses the entire cell relation, including the wraparound endpoint, not a weakened path equation.
```
lemma group_prefix_rotate {G : Type*} [Group G] {m : ℕ} (p : Fin m → G)
    (hp : (List.ofFn p).prod = 1) (i : Fin m) :
    ((List.ofFn p).take ((finRotate m i).val)).prod =
      ((List.ofFn p).take i.val).prod * p i := by
…
```
lemma OAI.HyperbolicObstruction.ConeSkeleton.frozenOffset_next line 42
lemma OAI.HyperbolicObstruction.ConeSkeleton.actualCellCover_frozen_closed line 64
Source documentation
Every indexed frozen face has its genuine closed lifted boundary, so the cover's closed-walk condition does not discard any actual lifted cell.
```
lemma actualCellCover_frozen_closed (g : G) (s : (frozenBoundary n w d).Side) :
    let H := actualCellCover n w d v hv hcell
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.frozenBoundary, OAI.HyperbolicObstruction.ConeSkeleton.actualCellCover