prev_eq'

Mathlib.Algebra.Homology.ComplexShape

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

← MathLib Explorer

English

If c.Rel i j holds, then c.prev j = i.

Русский

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

LaTeX

$$$c.Rel(i,j) \Rightarrow c.prev j = i$$$

Lean4

theorem prev_eq' (c : ComplexShape ι) {i j : ι} (h : c.Rel i j) : c.prev j = i :=
  by
  apply c.prev_eq _ h
  rw [prev, dif_pos]
  exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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