toFinset_singleton — Mathlib

English

The Finset representation of a singleton set {a} is the same singleton finset {a}: ({a} : Set α).toFinset = {a}.

Русский

Конечное множество-одиночка {a} в виде Finset совпадает с тем же самым Finset: ({a} : Set α).toFinset = {a}.

LaTeX

$$$\bigl\{a\bigr\} : Set\;\alpha\;\toFinset = \{a\}$$$

Lean4

@[simp]
theorem toFinset_singleton (a : α) [Fintype ({ a } : Set α)] : ({ a } : Set α).toFinset = { a } :=
  by
  ext
  simp

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