starEquivCostar_apply

Mathlib.Combinatorics.Quiver.Covering

URI: https://scilib.ai/kg/mathlib#Quiver.starEquivCostar_apply

English

The star–costar equivalence sends a Star.mk e to Costar.mk (reverse e).

Русский

Эквивалентность звезды и костара переводит Star.mk e в Costar.mk (обратный путь).

LaTeX

$$Quiver.starEquivCostar_apply$$

Lean4

@[simp]
theorem starEquivCostar_apply {u v : U} (e : u ⟶ v) :
    Quiver.starEquivCostar u (Quiver.Star.mk e) = Quiver.Costar.mk (reverse e) :=
  rfl

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

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

Разделы

Аффилиация

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