id_apply_one' — Mathlib

English

In the dependent formulation, the nth coefficient of id 𝕜 E is the identity when n = 1; more precisely, for x ∈ E, {n : ℕ}, and v : Fin n → E, we have (id 𝕜 E x) n v = v ⟨0, h.symm ▸ 0 < 1⟩ whenever n = 1.

Русский

В зависимой формулировке первый коэффициент id 𝕜 E есть тождественность: для x ∈ E, n = 1 и v : Fin n → E выполняется (id 𝕜 E x) n v = v 0.

LaTeX

$$$(id\\; \\mathbb{K}\\; E\\ x)_n(v) = v_0\\quad \\text{ whenever } n = 1$.$$

Lean4

/-- The `n`th coefficient of `id 𝕜 E` is the identity when `n = 1`. We state this in a dependent
way, as it will often appear in this form. -/
theorem id_apply_one' (x : E) {n : ℕ} (h : n = 1) (v : Fin n → E) : (id 𝕜 E x) n v = v ⟨0, h.symm ▸ zero_lt_one⟩ :=
  by
  subst n
  apply id_apply_one

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