English
The span of the family lapMatrix_ker_basis_aux G over all connected components fills the entire space of functions V → ℝ; i.e., the top subspace is contained in the real-span of these basis vectors.
Русский
Линейная оболочка семейства lapMatrix_ker_basis_aux G по всем связным компонентам заполняет все пространство функций V → ℝ; то есть верхнее подпространство содержится в линейной оболочке этих базисных векторов.
LaTeX
$$$$ \\top \\\\le \operatorname{span}_{\\mathbb{R}}\\bigl( \\operatorname{range}( \\mathrm{lapMatrix\\_ker\\_basis\\_aux}(G) ) \\bigr). $$$$
Lean4
theorem top_le_span_range_lapMatrix_ker_basis_aux : ⊤ ≤ Submodule.span ℝ (Set.range (lapMatrix_ker_basis_aux G)) :=
by
intro x _
rw [Submodule.mem_span_range_iff_exists_fun]
use Quot.lift x.val (by rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable, ← toLin'_apply, LinearMap.map_coe_ker])
ext j
simp only [lapMatrix_ker_basis_aux]
rw [AddSubmonoid.coe_finset_sum]
simp only [SetLike.mk_smul_mk, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, sum_ite_eq,
mem_univ, ↓reduceIte]
rfl
