{m : ℕ} (w : Fin m → E) (T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)) : LinearMap.range (whitened w T : EuclideanSpace ℂ (Fin m) →ₗ[ℂ] E) ≤ Submodule.span ℂ (Set.range w)

Initializing...

{m : ℕ} (w : Fin m → E) (T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)) : LinearMap.range (whitened w T : EuclideanSpace ℂ (Fin m) →ₗ[ℂ] E) ≤ Submodule.span ℂ (Set.range w) · Prove2Me