prev_eq_self'

Mathlib.Algebra.Homology.ComplexShape

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

English

If ∀ i, ¬ c.Rel i j, then prev j = j.

Русский

Если для всех i не выполняется c.Rel i j, тогда prev j = j.

LaTeX

$$\forall i, \lnot c.Rel i j \Rightarrow c.prev j = j$$

Lean4

theorem prev_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ i, ¬c.Rel i j) : c.prev j = j :=
  dif_neg (by simpa using hj)

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

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

Разделы

Аффилиация

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