coe_sort_coe — Mathlib

English

The type of elements of the set s, treated as a Set, is exactly the Finset s itself, i.e., the type of elements of s is canonically the same as s as a type.

Русский

Тип элементов множества s, рассматриваемый как множество, точно равен самому Finset s, то есть тип элементов s канонически совпадает с s как тип.

LaTeX

$$@[simp, norm_cast] theorem coe_sort_coe (s : Finset α) : ((s : Set α) : Sort _) = s := rfl$$

Lean4

@[simp, norm_cast]
theorem coe_sort_coe (s : Finset α) : ((s : Set α) : Sort _) = s :=
  rfl

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