CoreFan.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.CoreGeometry.IsFanVertex line 17
Source documentation
The actual vertices of the seven fan templates. The punctured D fan has only its two non-CD ports. All representatives of its point are retained.
```
def IsFanVertex (i : Fin 7) : Vertex → Prop
  | .inl r => pointOfRepresentative r = i
  | .inr l => Incident i l ∧ (i,l) ≠ (3,4)
```
Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex
instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 21) line 21
abbrev OAI.HyperbolicObstruction.CoreGeometry.FanVertex line 24
lemma OAI.HyperbolicObstruction.CoreGeometry.card_fanVertex line 26
lemma OAI.HyperbolicObstruction.CoreGeometry.card_fanVertex_le line 29
lemma OAI.HyperbolicObstruction.CoreGeometry.edge_fan_vertices line 32
def OAI.HyperbolicObstruction.CoreGeometry.FanAdjacent line 40
Source documentation
The undirected fan graph is a literal simple bipartite subgraph, not its quotient by letter labels (which need not be injective).
```
def FanAdjacent (i : Fin 7) (a b : FanVertex i) : Prop := Adjacent a.val b.val
```
Mentions: OAI.HyperbolicObstruction.CoreGeometry.FanVertex, OAI.HyperbolicObstruction.CoreGeometry.Adjacent
instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 41) line 41
def OAI.HyperbolicObstruction.CoreGeometry.linePart line 44
lemma OAI.HyperbolicObstruction.CoreGeometry.fanAdjacent_bipartite line 48
lemma OAI.HyperbolicObstruction.CoreGeometry.fanAdjacent_ne line 53
lemma OAI.HyperbolicObstruction.CoreGeometry.index_unique line 58
Source documentation
The edge index of a fan triangle is determined by its two radial labels. This is independent of coincident generator values in the random row.
```
lemma index_unique {e f : Edge} (h :
    ({Sum.inl e.val.1, .inr e.val.2} : Finset Vertex) =
      {Sum.inl f.val.1, .inr f.val.2}) : e = f := by
…
```
Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex