English
If a finite set u is contained in the scalar product s • t, there exist finite sets s' ⊆ s and t' ⊆ t such that u ⊆ s' • t'.
Русский
Если множество u содержится в скалярном произведении s • t, найдутся конечные подмножества s' ⊆ s и t' ⊆ t такие, что u ⊆ s' • t'.
LaTeX
$$$\text{If } \uparrow u \subseteq s \cdot t \text{ then } \exists s', t' : Finset,\; \uparrow s' \subseteq s \land \uparrow t' \subseteq t \land u \subseteq s' \cdot t'.$$$
Lean4
/-- If a finset `u` is contained in the scalar product of two sets `s • t`, we can find two finsets
`s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' • t'`. -/
@[to_additive /-- If a finset `u` is contained in the scalar sum of two sets `s +ᵥ t`, we can find two
finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' +ᵥ t'`. -/
]
theorem subset_smul {s : Set α} {t : Set β} :
↑u ⊆ s • t → ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t' :=
subset_set_image₂
