coe_eq_singleton — Mathlib

English

For any Finset s ⊆ α and any a ∈ α, the underlying set of s equals {a} if and only if s is the singleton {a}.

Русский

Для любого конечного множества s ⊆ α и любого a ∈ α выполняется: множество, полученное из s как множество, равно {a} тогда и только тогда, когда s = {a}.

LaTeX

$$$(s : \mathrm{Set} \alpha) = \{ a \} \iff s = \{ a \}$$$

Lean4

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

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