coe_toFinset

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Set.coe_toFinset

English

The set obtained by viewing toFinset s as a Set α is exactly s.

Русский

Множество, полученное как множество через приведение toFinset s к Set α, равно s.

LaTeX

$$$(s.toFinset)^{\uparrow} = s$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru