coe_fintypeCard

Mathlib.Data.Set.Card

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_fintypeCard (s : Set α) [Fintype s] : Fintype.card s = s.encard := by simp [encard_eq_coe_toFinset_card]

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

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

Разделы

Аффилиация

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