get_cons_nil — Mathlib

English

The single element of a one-element vector (x :: nil) is x for every index in Fin 1.

Русский

Едиственный элемент вектора длины 1 равен x для каждого индекса в Fin 1.

LaTeX

$$$\\forall {\\alpha} {ix : \\mathrm{Fin} 1} (x:\\alpha),\\; \\big(\\mathrm{cons}(x,\\mathrm{nil})\\big).get\\ ix = x$$$

Lean4

/-- Accessing the nth element of a vector made up
of one element `x : α` is `x` itself. -/
@[simp]
theorem get_cons_nil : ∀ {ix : Fin 1} (x : α), get (x ::ᵥ nil) ix = x
  | ⟨0, _⟩, _ => rfl

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