toFinset_ssubset — Mathlib

English

A strict Finset inclusion s.toFinset ⊂ t.toFinset holds if and only if s ⊂ t as multisets.

Русский

Строгое включение Finsets соответствует строгому включению мультимножеств.

LaTeX

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

Lean4

@[simp]
theorem toFinset_ssubset : s.toFinset ⊂ t.toFinset ↔ s ⊂ t :=
  by
  simp_rw [Finset.ssubset_def, toFinset_subset]
  rfl

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