truncationCompTrunc — Mathlib

English

For all natural numbers m ≤ n, the truncation at level n factors through truncation at level m, establishing a canonical isomorphism between the composed truncations: truncation n ∘ Truncated.trunc C n m h ≅ truncation m.

Русский

Для всех m ≤ n усечение на уровне n факторизуется через усечение на уровне m, образуя каноническое изоморфизм между составными усечениями: truncation n ∘ Truncated.trunc C n m h ≅ truncation m.

LaTeX

$$$$ \\forall \\{m,n:\\mathbb{N}\\}, (h: m \\le n) \\Rightarrow \\ truncation\\ n \\;\\circ\\; Truncated.trunc\\ C\\ n\\ m\\ h \\;\\cong\\; truncation\\ m $$$$

Lean4

/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`. -/
def truncationCompTrunc {n m : ℕ} (h : m ≤ n) : truncation n ⋙ Truncated.trunc C n m ≅ truncation m :=
  Iso.refl _

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