card_eq_of_equiv

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Finset.card_eq_of_equiv

English

If i : s ≃ t, then card s = card t.

Русский

Если i : s ≃ t, тогда card s = card t.

LaTeX

$${i : s ≃ t} → |s| = |t|$$

Lean4

theorem card_eq_of_equiv {s : Finset α} {t : Finset β} (i : s ≃ t) : #s = #t :=
  (card_eq_of_equiv_fintype i).trans (Fintype.card_coe _)

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

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

Разделы

Аффилиация

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