subset_vsub — Mathlib

English

If a finite set u is contained in the pointwise difference s -ᵥ t of sets s and t, then there exist finite 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 pointwise subtraction of two sets `s -ᵥ t`, we can find two
finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' -ᵥ t'`. -/
theorem subset_vsub {s t : Set β} : ↑u ⊆ s -ᵥ t → ∃ s' t' : Finset β, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t' :=
  subset_set_image₂

Похожие утверждения