card_eq_iff_eq_univ

Mathlib.Data.Fintype.Card

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

← MathLib Explorer

English

For finite α, #s = Fintype.card α iff s = univ.

Русский

Для конечного α: #s = Fintype.card α тогда и только тогда, когда s = univ.

LaTeX

$$$ #s = \\operatorname{Fintype.card} α \\;\\Leftrightarrow\\; s = \\mathrm{univ}. $$$

Lean4

theorem card_eq_iff_eq_univ [Fintype α] (s : Finset α) : #s = Fintype.card α ↔ s = univ :=
  ⟨s.eq_univ_of_card, by
    rintro rfl
    exact Finset.card_univ⟩

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

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

Разделы

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

Аффилиация

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