card_attachFin

Mathlib.Data.Finset.Fin

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

English

The cardinality is preserved by attachFin: (s.attachFin h).card = s.card.

Русский

Кардинальность сохраняется при attachFin: (s.attachFin h).card = s.card.

LaTeX

$$(s.attachFin h).card = s.card$$

Lean4

@[simp]
theorem card_attachFin (s : Finset ℕ) (h : ∀ m ∈ s, m < n) : (s.attachFin h).card = s.card :=
  Multiset.card_pmap _ _ _

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

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

Разделы

Аффилиация

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