prev_f

Mathlib.Algebra.Homology.Embedding.Boundary

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.prev_f

English

If c.prev j = i, then the image under e of the previous element equals the previous image, given IsTruncLE.

Русский

Если c.prev j = i, тогда e(f(j)) prev = e(f(i)) при условии IsTruncLE.

LaTeX

$$Prev_f [e.IsTruncLE] {i j} (hij: c.prev j = i) : c'.prev (e.f j) = e.f i$$

Lean4

theorem prev_f [e.IsTruncLE] {i j : ι} (hij : c.prev j = i) : c'.prev (e.f j) = e.f i :=
  e.op.next_f hij

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

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

Разделы

Аффилиация

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