English
If a Finite set u is contained in the pointwise division s / t for sets s and t, then there exist finite subsets s' ⊆ s and t' ⊆ t such that u ⊆ s' / t'.
Русский
Если конечный набор u содержится в точечном делении u ⊆ s/t для множеств s и t, существуют конечные подмножества s' ⊆ s и t' ⊆ t такие, что u ⊆ s'/t'.
LaTeX
$$$$ u \\subseteq s/t \\Rightarrow \\exists s',t' : Finset α, s' \\subseteq s \\land t' \\subseteq t \\land u \\subseteq 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_div {s t : Set α} : ↑u ⊆ s / t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t' :=
subset_set_image₂
