nil_append_iff

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

The walk p.append q is Nil iff both p and q are Nil.

Русский

Ход p.append q равен Nil тогда, когда оба хода p и q равны Nil.

LaTeX

$$$ (p.append q).Nil \iff p.Nil \land q.Nil $$$

Lean4

@[simp]
theorem nil_append_iff {p : G.Walk u v} {q : G.Walk v w} : (p.append q).Nil ↔ p.Nil ∧ q.Nil := by
  cases p <;> cases q <;> simp

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

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

Разделы

Аффилиация

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