trunc_spine — Mathlib

English

If X is truncated above level n+1, then the m-spine is unchanged by truncation at level k+1, provided m ≤ n+1 and k ≤ n.

Русский

Если X усечено выше уровня n+1, тогда m-спайн не изменяется при усечении на уровне k+1 при условии m ≤ n+1 и k ≤ n.

LaTeX

$$$\forall X (k,m : \mathbb{N}), (h : m \le n+1) (h_n : k \le n),\ ((\mathrm{trunc}(n+1)(k+1)).\mathrm{obj} X).\mathrm{spine} \\! m = X.\mathrm{spine} \\! m$$$

Lean4

/-- Further truncating `X` above `m` does not change the `m`-spine. -/
theorem trunc_spine (k m : ℕ) (h : m ≤ k + 1) (hₙ : k ≤ n) : ((trunc (n + 1) (k + 1)).obj X).spine m = X.spine m :=
  rfl

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