coe_eq_pair — Mathlib

English

For any s, a, b, the underlying set of {a, b} is {a, b}, and the card is determined accordingly.

Русский

У множества {a,b} как множества надлежащая оболочка совпадает с {a,b}.

LaTeX

$$${s : Finset \\alpha} \\ {a,b} : (({a,b} : Finset \\alpha) : Set \\alpha) = {a,b}$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_pair {s : Finset α} {a b : α} : (s : Set α) = { a, b } ↔ s = { a, b } := by rw [← coe_pair, coe_inj]

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