fintype — Mathlib

English

If a path p is Hamiltonian, then the vertex set α is finite.

Русский

Если путь p Гамильтониан, то множество вершин α конечно.

LaTeX

$$$$p.IsHamiltonian \Rightarrow \text{Fintype }\alpha.$$$$

Lean4

/-- If a path `p` is Hamiltonian then its vertex set must be finite. -/
protected def fintype (hp : p.IsHamiltonian) : Fintype α
    where
  elems := p.support.toFinset
  complete x := List.mem_toFinset.mpr (mem_support hp x)

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