finsetEquivSet_apply

Mathlib.Data.Fintype.Sets

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

English

The forward application of finsetEquivSet to a Finset s yields s viewed as a Set, i.e., finsetEquivSet s = s.

Русский

Прямое применение финсетEquivSet к Finset s дает тот же множества как множество: finsetEquivSet s = s.

LaTeX

$$$\mathrm{finsetEquivSet}\;s = s$$$

Lean4

@[simp]
theorem finsetEquivSet_apply (s : Finset α) : finsetEquivSet s = s :=
  rfl

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

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

Разделы

Аффилиация

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