snocCases_snoc — Mathlib

English

If x is injective and x0 is not in its range, then snoc x x0 is injective.

Русский

Если x инъективна и x0 не лежит в её образе, то snoc x x0 инъективна.

LaTeX

$$$\\\\text{snoc}_{x,x_0} \\text{ injective} \\;\\Rightarrow \\\\text{injective}(snoc x x_0)$$$

Lean4

@[simp]
theorem snocCases_snoc {P : (∀ i : Fin (n + 1), α i) → Sort*} (h : ∀ x x₀, P (Fin.snoc x x₀))
    (x : ∀ i : Fin n, (Fin.init α) i) (x₀ : α (Fin.last _)) : snocCases h (Fin.snoc x x₀) = h x x₀ := by
  rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]

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