instIsTruncGEEmbeddingUp'Add

Mathlib.Algebra.Homology.Embedding.Basic

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

English

For the embedding UpAdd construction, if c'.Rel(e.f j, k') holds, there exists k with e.f k = k'.

Русский

Для вложения UpAdd существует k, если c'.Rel( e.f j, k') держится.

LaTeX

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

Lean4

instance (a b : A) : (embeddingUp'Add a b).IsTruncGE where mem_next {j _} h := ⟨j + a, (add_right_comm _ _ _).trans h⟩

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

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

Разделы

Аффилиация

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