finsetEquivSet_symm_apply

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Fintype.finsetEquivSet_symm_apply

English

The inverse map sends a Set s to its Finset representation: finsetEquivSet.symm s = s.toFinset.

Русский

Обратная карта отправляет множество s в его представление как Finset: finsetEquivSet.symm s = s.toFinset.

LaTeX

$$$\mathrm{finsetEquivSet}.symm\;s = s.toFinset$$$

Lean4

@[simp]
theorem finsetEquivSet_symm_apply (s : Set α) [Fintype s] : finsetEquivSet.symm s = s.toFinset := by
  simp [finsetEquivSet]

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

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

Разделы

Аффилиация

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