encard_eq_coe_toFinset_card

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

If s is finite, then encard s equals the Finset s.card cast to ENat.

Русский

Если s конечно, то encard s равно card Finset s, приведённому в ENat.

LaTeX

$$$ s.encard = (\operatorname{toFinset}(s).card).cast $$$

Lean4

theorem encard_eq_coe_toFinset_card (h : s.Finite) : s.encard = h.toFinset.card :=
  by
  have := h.fintype
  rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]

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

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

Разделы

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

Аффилиация

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