support_toFinset — Mathlib

English

The support of a Hamiltonian walk equals the entire vertex set as a Finset.

Русский

Поддержка гамильтонова маршрута равна полному множеству вершин как Finset.

LaTeX

$$$$p.IsHamiltonian \Rightarrow p.support.toFinset = \text{Finset.univ}.$$$$

Lean4

/-- The support of a Hamiltonian walk is the entire vertex set. -/
theorem support_toFinset (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ := by simp [eq_univ_iff_forall, hp]

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