toFinset_subset_toFinset — Mathlib

English

For any finite s and Finset t, s.toFinset ⊆ t.toFinset iff s ⊆ t as sets.

Русский

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

LaTeX

$$$s.toFinset \subseteq t.toFinset \iff s \subseteq t$$$

Lean4

@[mono]
theorem toFinset_subset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊆ t.toFinset ↔ s ⊆ t := by
  simp [Finset.subset_iff, Set.subset_def]

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