truncationCompTrunc — Mathlib

English

For all m ≤ n, the composition truncation_n followed by truncation through n of level m is canonically isomorphic to truncation_m.

Русский

Для всех m ≤ n композиция truncation_n далее Truncated.trunc(n,m) изоморфна по канону к truncation_m.

LaTeX

$$$\mathrm{truncation}_n \;\circ\; \mathrm{Truncated.trunc}_{n,m} \cong \mathrm{truncation}_m \quad (m \le n)$$$

Lean4

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

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