PictureMapFurther.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.restrict line 21
Source documentation
A union of whole polygonal components can be kept, discarding the others. This is a literal restriction of both permutations.
```
def restrict (hf : ∀ x, P (M.face x) ↔ P x) (he : ∀ x, P (M.edge x) ↔ P x) :
    PictureMap (Subtype P) where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.restrict_vertex line 33
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.restrict_components line 38
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.component_invariant line 50
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_split line 56
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.card_darts_even line 66

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler_split line 73

Source documentation

The Euler characteristic is additive over actual invariant dart subsets.

theorem euler_split (hf : ∀ x, P (M.face x) ↔ P x) (he : ∀ x, P (M.edge x) ↔ P x) :
    M.euler = (M.restrict P hf he).euler + (M.restrict (fun x => ¬ P x)
      (fun x => not_congr (hf x)) (fun x => not_congr (he x))).euler := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.restrict_genusZero line 94
Source documentation
Discarding components of a genus-zero picture preserves genus zero. This justifies keeping the disk component and deleting sphere components after crosswise switches, at the level of the actual finite side-pairing.
```
theorem restrict_genusZero (hM : M.GenusZero)
    (hf : ∀ x, P (M.face x) ↔ P x) (he : ∀ x, P (M.edge x) ↔ P x) :
    (M.restrict P hf he).GenusZero := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero