subset_toFinset — Mathlib

English

For a Finset s, s ⊆ t.toFinset iff ↑s ⊆ t, where ↑s is the underlying Set.

Русский

Для Finset s верно, что s ⊆ t.toFinset тогда и только тогда ↑s ⊆ t, где ↑s — соответствующее множество.

LaTeX

$$$s \subseteq t^{\mathrm{toFinset}} \iff \uparrow s \subseteq t$$$

Lean4

@[simp]
theorem subset_toFinset {s : Finset α} [Fintype t] : s ⊆ t.toFinset ↔ ↑s ⊆ t := by
  rw [← Finset.coe_subset, coe_toFinset]

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