encard_coe_eq_coe_finsetCard

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

For a Finset s, encard (s : Set α) equals s.card.

Русский

Для Finset s, encard (s : Set α) равно s.card.

LaTeX

$$$ encard (s : Set α) = s.card $$$

Lean4

@[simp, norm_cast]
theorem encard_coe_eq_coe_finsetCard (s : Finset α) : encard (s : Set α) = s.card := by
  rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]; simp

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

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

Разделы

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

Аффилиация

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