instFintypeSimpleGraphOfDecidableEq

English

There are finitely many simple graphs on a finite vertex set V.

Русский

Для заданного конечного множества вершин V существует конечное число простых графов на V.

LaTeX

$$$ | \mathrm{SimpleGraph}(V)\,| < \infty $$$

Lean4

/-- We can enumerate simple graphs by enumerating all functions `V → V → Bool`
and filtering on whether they are symmetric and irreflexive. -/
instance {V : Type u} [Fintype V] [DecidableEq V] : Fintype (SimpleGraph V)
    where
  elems := Finset.univ.map SimpleGraph.mk'
  complete := by
    classical
    rintro ⟨Adj, hs, hi⟩
    simp only [mem_map, mem_univ, true_and, Subtype.exists, Bool.not_eq_true]
    refine ⟨fun v w ↦ Adj v w, ⟨?_, ?_⟩, ?_⟩
    · simp [hs.iff]
    · intro v; simp [hi v]
    · ext
      simp

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