toFinset_coe — Mathlib

English

For any Finset s, the Set coerced from s and then turned back into a Finset returns the original Finset: (s : Set α).toFinset = s.

Русский

Для любого Finset s множество, полученное за его приведение к типу Set и обратно в Finset, равно исходному Finset: (s : Set α).toFinset = s.

LaTeX

$$$ (s : Set\;\alpha).toFinset = s $$$

Lean4

@[simp]
theorem toFinset_coe (s : Finset α) [Fintype (s : Set α)] : (s : Set α).toFinset = s :=
  ext fun _ => Set.mem_toFinset

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