setOf_mem_eq_empty_iff — Mathlib

English

The set of elements belonging to a list is empty iff the list is empty.

Русский

Множество элементов, принадлежащих списку, пусто тогда и только тогда, когда список пуст.

LaTeX

$$$\\forall {\\\\alpha} {l : List \\\\alpha}, {x \\;|\; x \\\\in l} = \\\\emptyset \\\\Leftrightarrow l = []$$$

Lean4

@[simp]
theorem setOf_mem_eq_empty_iff {l : List α} : {x | x ∈ l} = ∅ ↔ l = [] :=
  Set.eq_empty_iff_forall_notMem.trans eq_nil_iff_forall_not_mem.symm

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