Model.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Barnette.PlaneEmbedding line 10
Source documentation
A topological plane drawing of a simple graph, with no crossings.
Also declared: ComparatorChallenges/BarnetteHamiltonian.lean:10 (same declaration text).
```
structure PlaneEmbedding {V : Type u} (G : SimpleGraph V) where
…
```
def OAI.Barnette.Planar line 29
Source documentation
Planarity means existence of a crossing-free topological plane embedding.
Also declared: ComparatorChallenges/BarnetteHamiltonian.lean:29 (same declaration text).
```
def Planar {V : Type u} (G : SimpleGraph V) : Prop :=
…
```
def OAI.Barnette.ThreeVertexConnected line 33
Source documentation
Deleting any set of at most two vertices leaves a connected graph of order at least two.
Also declared: ComparatorChallenges/BarnetteHamiltonian.lean:33 (same declaration text).
```
def ThreeVertexConnected {V : Type u} [Fintype V] (G : SimpleGraph V) : Prop :=
…
```
def OAI.Barnette.HasHamiltonianCycle line 38
Source documentation
A single spanning cycle, not a possibly disconnected spanning 2-factor.
Also declared: ComparatorChallenges/BarnetteHamiltonian.lean:38 (same declaration text).
```
def HasHamiltonianCycle {V : Type u} [DecidableEq V] (G : SimpleGraph V) : Prop :=
…
```
def OAI.Barnette.MainStatement line 42
Source documentation
Cubic bipartite three-vertex-connected plane graphs have a Hamiltonian cycle.
Also declared: ComparatorChallenges/BarnetteHamiltonian.lean:42 (same declaration text).
```
def MainStatement : Prop :=
…
```