OAI/Topology/ArtinGroups/ParabolicIntersections/VisualAmalgamProperties.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The nondegeneracy and edge-identification hypotheses of the published amalgam criterion, verified for the actual Artin visual splitting.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_edge_comap line 14
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_edge_inclusion_proper line 33