toFinset_card

Mathlib.Data.Fintype.Card

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

← MathLib Explorer

English

For a set s, the card of s.toFinset equals Fintype.card s.

Русский

Для множества s кардинал s.toFinset равен Fintype.card s.

LaTeX

$$$ s^{\\mathrm{toFinset}}.card = \\operatorname{Fintype.card} s. $$$

Lean4

@[simp]
theorem toFinset_card {α : Type*} (s : Set α) [Fintype s] : s.toFinset.card = Fintype.card s :=
  Multiset.card_map Subtype.val Finset.univ.val

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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