coe_singleton — Mathlib

English

Let α be a type and a ∈ α. The set obtained by viewing the singleton finset {a} as a subset of α is exactly {a}.

Русский

Пусть α — множество, и элемент a ∈ α. Множество, получаемое приведением одноэлементного множества {a} к множеству α, равно {a}.

LaTeX

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

Lean4

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

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