toFinset_subset — Mathlib

English

For any s,t, the Finset s.toFinset is a subset of t.toFinset if and only if s is a subset of t (as multisets).

Русский

Для мультимножестваs и t справедливо: s.toFinset ⊆ t.toFinset тогда и только тогда, когда s ⊆ t как мультимножества.

LaTeX

$$$\\forall {s t : \\mathsf{Multiset}\\,\\alpha}, s.toFinset \\subseteq t.toFinset \\iff s \\subseteq t$$$

Lean4

@[simp]
theorem toFinset_subset : s.toFinset ⊆ t.toFinset ↔ s ⊆ t := by
  simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

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