$A \otimes B = (A \otimes W) \cap (V \otimes B)$ for subspaces over a field

Let $\mathbb{K}$ be a field and let $V, W$ be vector spaces over $\mathbb{K}$. For subspaces $A \subseteq V$ and $B \subseteq W$ write $A \otimes B$ for the subspace of $V \otimes_{\mathbb{K}} W$ spanned by the pure tensors $a \otimes b$ with $a \in A$, $b \in B$. In Lean this subspace is Mathlib's LinearMap.range (TensorProduct.mapIncl A B), the image of the map $A \otimes B \to V \otimes W$ induced by the two inclusions. For every subspace $A \subseteq V$ and $B \subseteq W$,

This reduces intersections of tensor products of subspaces to the one-sided subspaces $A \otimes W$ and $V \otimes B$, and is the main step towards the factorwise intersection formula QLLL.TensorProduct.range_mapIncl_inf_range_mapIncl. It is also used to identify extended constraints in the tensor-product form of the $k$-QSAT corollary.

Formalization Note No finite-dimensionality is assumed. On the platform the name carries a QLLL. prefix so that it cannot clash with Mathlib if an equivalent lemma is added there later.