support_nonempty

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.support_nonempty

English

The set {w | w ∈ p.support} is nonempty.

Русский

Множество {w | w ∈ p.support} непусто.

LaTeX

$$$\{ w \mid w \in p.\mathrm{support} \}.\mathrm{Nonempty}$$$

Lean4

@[simp]
theorem support_nonempty {u v : V} (p : G.Walk u v) : {w | w ∈ p.support}.Nonempty :=
  ⟨u, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru