encard_eq_coe_toFinset_card

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

For s : Set α with [Fintype s], encard s equals s.toFinset.card cast to ENat.

Русский

Для s : Set α с инстантом Fintype encard s равен s.toFinset.card.cast.

LaTeX

$$$ encard\,s = (s.toFinset.card).cast $$$

Lean4

theorem encard_eq_coe_toFinset_card (s : Set α) [Fintype s] : encard s = s.toFinset.card :=
  by
  have h := toFinite s
  rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]

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

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

Разделы

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

Аффилиация

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