mapPath_id

Mathlib.Combinatorics.Quiver.Path

URI: https://scilib.ai/kg/mathlib#Prefunctor.mapPath_id

Lean4

@[simp]
theorem mapPath_id {a b : V} : (p : Path a b) → (𝟭q V).mapPath p = p
  | Path.nil => rfl
  | Path.cons q e => by dsimp; rw [mapPath_id q]

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

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

Разделы

Аффилиация

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