OAI/Combinatorics/Ramsey/CycleClique/Construction/SmallCycleGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact short-cycle constructions and exterior-neighbour counts for Section 4.

  1. theorem OAI.CycleClique.Construction.hasCycle_of_closed_list line 9
  2. theorem OAI.CycleClique.Construction.hasCycle_four_of_edges line 24
  3. theorem OAI.CycleClique.Construction.hasCycle_five_of_edges line 36
  4. def OAI.CycleClique.Construction.exteriorNeighbors line 43
  5. theorem OAI.CycleClique.Construction.mem_exteriorNeighbors line 48
  6. theorem OAI.CycleClique.Construction.exteriorNeighbors_card_lower line 54
  7. theorem OAI.CycleClique.Construction.fourCycle_triangle_exterior_disjoint line 74

    Source documentation

    Outside a triangle, a common neighbour of two triangle vertices creates a four-cycle.

    theorem fourCycle_triangle_exterior_disjoint {V : Type*} [Fintype V]
    {G : SimpleGraph V} {Q : Finset V} (hQ : G.IsClique (Q : Set V)) (hQcard : Q.card = 3)
    (hcycle : ¬ HasCycle G 4) {x y : V} (hx : x ∈ Q) (hy : y ∈ Q) (hxy : x ≠ y) :
    Disjoint (exteriorNeighbors G Q x) (exteriorNeighbors G Q y) := by
…

    Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.exteriorNeighbors

  8. theorem OAI.CycleClique.Construction.fourCycle_triangle_exterior_anticomplete line 92

    Source documentation

    Edges between two triangle exterior classes create a four-cycle.

    theorem fourCycle_triangle_exterior_anticomplete {V : Type*} [Fintype V]
    {G : SimpleGraph V} {Q : Finset V} (hQ : G.IsClique (Q : Set V))
    (hcycle : ¬ HasCycle G 4) {x y u v : V}
    (hx : x ∈ Q) (hy : y ∈ Q) (hxy : x ≠ y)
    (hu : u ∈ exteriorNeighbors G Q x) (hv : v ∈ exteriorNeighbors G Q y) :
    ¬ G.Adj u v := by
…

    Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.exteriorNeighbors