card_eq_card_toFinset

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_eq_card_toFinset

English

Let s be a subset of α with [Fintype s]. Then Nat.card s = s.toFinset.card.

Русский

Пусть s ⊆ α и [Fintype s]. Тогда Nat.card s = s.toFinset.card.

LaTeX

$$$ \forall s : \mathrm{Set}\,\alpha, [\mathrm{Fintype}\,s], \ \mathrm{Nat.card}\,s = s.toFinset.card $$$

Lean4

theorem card_eq_card_toFinset (s : Set α) [Fintype s] : Nat.card s = s.toFinset.card := by
  simp only [← Nat.card_eq_finsetCard, s.mem_toFinset]

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

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

Разделы

Аффилиация

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