ncard_eq_toFinset_card'

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.ncard_eq_toFinset_card'

← MathLib Explorer

English

If s is finite, then ncard s equals the cardinality of its finite set representation.

Русский

Если s конечное, то ncard s равна кардинальности его представления как конечного множества.

LaTeX

$$$ s.ncard = s.toFinset.card $$$

Lean4

theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] : s.ncard = s.toFinset.card := by
  simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]

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

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

Разделы

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

Аффилиация

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