Proof of `Dimension and component-rank bounds for effective test spaces` (3rd statement)
groundedproofs/Lax342547Proofs/EffectiveBounds.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The range of every tensor matrix is contained in its first factor space. Apply the same argument to the transpose to bound the rank by the second factor as well.