map_id — Mathlib

English

The map composed from i to i+1 and then back to i reduces to the identity at i.

Русский

Отображение, пройденное по шагу i → i+1 затем обратно обратно к i, сводится к тождественному морфизму на i.

LaTeX

$$$\\forall i,\\ map f i i (by \\\\ cutsat) = \\mathrm{Id}_{X_i}.$$$

Lean4

theorem map_id (i : ℕ) : map f i i (by cutsat) = 𝟙 _ :=
  by
  revert X f
  induction i with
  | zero => intros; rfl
  | succ _ hi =>
    intro X f
    apply hi

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