English
Let v be a linearly independent family with top spanning property hsp, and form the basis B = Basis.mk hli hsp. Then the representation map of B evaluated at x equals the representation of the original independent family applied to the pair (x, proof that x ∈ ⊤).
Русский
Пусть v — линейно независимая система и множество, порождённое ею, покрывает все пространство, тогда базис B = Basis.mk hli hsp имеет представление, удовлетворяющее B.repr x = hli.repr ⟨x, hsp Submodule.mem_top⟩.
LaTeX
$$$(Basis.mk\\ hli\\ hsp).repr\\ x = hli.repr\\langle x, hsp\\ Submodule.mem\\_top\\rangle$$$
Lean4
@[simp]
theorem mk_repr : (Basis.mk hli hsp).repr x = hli.repr ⟨x, hsp Submodule.mem_top⟩ :=
rfl
