instIsTruncLENatIntEmbeddingUpIntLE

English

The LE version, embeddingUpIntLE, inherits a generalized truncation property, mirroring the GE counterpart for the LE construction.

Русский

Версия LE вложения UpIntLE наследует обобщённое свойство усечения, повторяющее GE-аналоги для конструкции LE.

LaTeX

$$$(embeddingUpIntLE(p)).IsTruncGE$ and $ (embeddingUpIntLE(p)).IsTruncLE$$$

Lean4

instance : (embeddingUpIntLE p).IsTruncLE where mem_prev {_ k} h := ⟨k + 1, by dsimp at h ⊢; omega⟩

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