mem_next

Mathlib.Algebra.Homology.Embedding.Basic

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

English

If j is a parameter and k' is in the target index, then there exists k with e.f k = k'.

Русский

Если j — параметр, а k' принадлежит целочисленной метке, существует k такой, что e.f k = k'.

LaTeX

$$$\\exists k,\, e.f\\, k = k' $$$

Lean4

theorem mem_next [e.IsTruncGE] {j : ι} {k' : ι'} (h : c'.Rel (e.f j) k') : ∃ k, e.f k = k' :=
  IsTruncGE.mem_next h

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

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

Разделы

Аффилиация

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