instIsTruncLEEmbeddingDown'Add

Mathlib.Algebra.Homology.Embedding.Basic

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

English

The natural embedding from up ℕ to up ℤ preserves the RelIff property.

Русский

Естественное вложение from up ℕ в up ℤ сохраняет свойство RelIff.

LaTeX

$$$(ComplexShape.embeddingUpNat).IsRelIff$$$

Lean4

instance (a b : A) : (embeddingDown'Add a b).IsTruncLE where mem_prev {_ x} h := ⟨x + a, (add_right_comm _ _ _).trans h⟩

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

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

Разделы

Аффилиация

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