GraphConjecture315.lean`

8 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 315

Reference:E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Definitions

The notions IsTotalDominatingSet, IsMinimalTotalDominatingSet, IsWellTotallyDominated, and pendantVertices live in FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.WellTotallyDominated.

Imports (1)

FormalConjecturesUtil

theorem WrittenOnTheWallII.GraphConjecture315.conjecture315 sorry line 53 source
depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Eq, Nat, SimpleGraph.indepNum, Finset.card, SimpleGraph.pendantVertices, SimpleGraph.IsWellTotallyDominated
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
example WrittenOnTheWallII.GraphConjecture315.(example at line 63) line 63 source
Source documentation
In the path graph $P_3$ ($0$-$1$-$2$), vertices $0$ and $2$ have degree $1$, so there are exactly $2$ pendant vertices.
```
example : (pendantVertices (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3))).card = 2 := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 69) line 69 source
Source documentation
In $K_3$, all vertices have degree $2$, so there are no pendant vertices.
```
example : (pendantVertices (⊤ : SimpleGraph (Fin 3))).card = 0 := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 75) line 75 source
Source documentation
In $K_2$, both vertices have degree $1$, so both are pendant vertices.
```
example : (pendantVertices (⊤ : SimpleGraph (Fin 2))).card = 2 := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 81) line 81 source
Source documentation
In $K_2$, the pendant set is exactly $\{0, 1\}$.
```
example : pendantVertices (⊤ : SimpleGraph (Fin 2)) = Finset.univ := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 87) line 87 source
Source documentation
In the edgeless graph on $3$ vertices, no vertex has degree $1$, so there are $0$ pendant vertices.
```
example : (pendantVertices (⊥ : SimpleGraph (Fin 3))).card = 0 := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 93) line 93 source
Source documentation
$\{0, 1\}$ is a total dominating set of $K_2$: every vertex has a neighbor in $\{0, 1\}$.
```
example : IsTotalDominatingSet (⊤ : SimpleGraph (Fin 2)) Finset.univ := by
…
```
example WrittenOnTheWallII.GraphConjecture315.(example at line 101) line 101 source
Source documentation
$\{0, 1\}$ is NOT a total dominating set of the edgeless graph on $2$ vertices, since no vertex has a neighbor in the empty edge set.
```
example : ¬IsTotalDominatingSet (⊥ : SimpleGraph (Fin 2)) Finset.univ := by
…
```