isIndepSet_neighborSet_of_triangleFree

English

The neighbors of a vertex form an independent set in a triangle-free graph.

Русский

Соседи вершины образуют независимое множество в графе без треугольников.

LaTeX

$$$\\text{If } G\\text{ is triangle-free},\\ G.isIndepSet( G.neighborSet(v) ).$$$

Lean4

/-- The neighbors of a vertex `v` form an independent set in a triangle free graph `G`. -/
theorem isIndepSet_neighborSet_of_triangleFree (h : G.CliqueFree 3) (v : α) : G.IsIndepSet (G.neighborSet v) := by
  classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push_neg at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h { v, j, k } (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))

Похожие утверждения