insertNthEquiv_last — Mathlib

English

Equivalence with the last-index variant coincides with the standard snoc-based equivalence.

Русский

Эквивалентность для последнего индекса совпадает с обычной эквивалентностью на основе snoc.

LaTeX

$$$$ \mathrm{insertNthEquiv}\ (\lambda\_\mapsto α)\ (\mathrm{last}\ n) = \mathrm{snocEquiv}\ (\lambda\_\mapsto α) $$$$

Lean4

/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality. -/
@[simp]
theorem insertNthEquiv_last (n : ℕ) (α : Type*) : insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α) := by ext;
  simp

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