toFinset_vsub — Mathlib

English

For sets s ⊆ β and t ⊆ β, the Finset corresponding to the pointwise difference s -ᵥ t equals Finset.vsub of the Finsets: (s -ᵥ t).toFinset = Finset.vsub.vsub s.toFinset t.toFinset.

Русский

Для множеств s и t верно: (s -ᵥ t).toFinset = Finset.vsub.vsub s.toFinset t.toFinset.

LaTeX

$$$(s -ᵥ t)^{\\!\\toFinset} = (s^{\\!\\toFinset} -ᵥ t^{\\!\\toFinset})$$$

Lean4

@[simp]
theorem toFinset_vsub (s t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s -ᵥ t)] :
    (s -ᵥ t : Set α).toFinset = s.toFinset -ᵥ t.toFinset :=
  toFinset_image2 _ _ _

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