val_toFinset — Mathlib

English

For any Finset s, the Finset obtained from its carrier as a multiset equals s itself.

Русский

Для любого финсетa s финсет, образованный из его множества может быть получен как s.

LaTeX

$$$\\forall s : \\mathsf{Finset}\\,\\alpha,\\; s.\\mathrm{val}.toFinset = s$$$

Lean4

@[simp]
theorem val_toFinset [DecidableEq α] (s : Finset α) : s.val.toFinset = s :=
  by
  ext
  rw [Multiset.mem_toFinset, ← mem_def]

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