apply_eq_iff — Mathlib

English

Define a basis by mapping each vector to its coordinates via a finite-linear isomorphism e: M ≃ₗ[R] ι → R.

Русский

Определим базис через отображение каждого вектора в его координаты по линейному эквиваленту e: M ≃ₗ[R] ι → R.

LaTeX

$$$$ Basis.ofEquivFun\, e : Basis\, ι\, R\, M $$$$

Lean4

theorem apply_eq_iff {b : Basis ι R M} {x : M} {i : ι} : b i = x ↔ b.repr x = Finsupp.single i 1 :=
  ⟨fun h => h ▸ b.repr_self i, fun h => b.repr.injective ((b.repr_self i).trans h.symm)⟩

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