coe_eq_empty — Mathlib

English

Let s be a finite set of α. The underlying set of elements of s is empty if and only if s is the empty set.

Русский

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

LaTeX

$$$ (s : Set \alpha) = \emptyset \iff s = \emptyset $$$

Lean4

@[simp, norm_cast]
theorem coe_eq_empty {s : Finset α} : (s : Set α) = ∅ ↔ s = ∅ := by grind

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