English
If a finite set u is contained in the product s * t of two sets s and t, there exist finite subsets s' ⊆ s and t' ⊆ t such that u ⊆ s' * t'.
Русский
Если конечное множество u ⊆ s·t, то существуют конечные подмножества s' ⊆ s и t' ⊆ t такие, что u ⊆ s' * t'.
LaTeX
$${s t : Set α} : ↑u ⊆ s * t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'$$
Lean4
/-- If a finset `u` is contained in the 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 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_mul {s t : Set α} : ↑u ⊆ s * t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t' :=
subset_set_image₂
