next_eq_self'

Mathlib.Algebra.Homology.ComplexShape

URI: https://scilib.ai/kg/mathlib#ComplexShape.next_eq_self'

English

If there are no outgoing relations from j, i.e., ∀ k, not c.Rel j k, then next j = j.

Русский

Если у j нет исходящих отношений, то next j = j.

LaTeX

$$\forall k, \lnot c.Rel j k \Rightarrow c.next j = j$$

Lean4

theorem next_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ k, ¬c.Rel j k) : c.next j = j :=
  dif_neg (by simpa using hj)

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

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

Разделы

Аффилиация

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