toList_eq_nil — Mathlib

English

Let s be a finite set. The list of its elements is empty if and only if s is the empty finset.

Русский

Пусть s — конечное множество. Список элементов s пуст тогда и только тогда, когда s = ∅.

LaTeX

$$$\\\\forall s : \\\\mathrm{Finset}\\\\,\\\\alpha,\\\\ s\\\\.toList = [] \\\\iff \\\\ s = \\\\emptyset$$$

Lean4

@[simp]
theorem toList_eq_nil {s : Finset α} : s.toList = [] ↔ s = ∅ :=
  Multiset.toList_eq_nil.trans val_eq_zero

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