eq_univ_of_card

Mathlib.Data.Fintype.Card

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

← MathLib Explorer

English

If p is a finset fin, then eq_univ_of_card states equality of cardinals implies equality of sets.

Русский

Если кардинал равен, то множества равны.

LaTeX

$$$ s = \\mathrm{univ} \\quad \\text{if } #s = \\operatorname{Fintype.card} α. $$$

Lean4

theorem eq_univ_of_card [Fintype α] (s : Finset α) (hs : #s = Fintype.card α) : s = univ :=
  eq_of_subset_of_card_le (subset_univ _) <| by rw [hs, Finset.card_univ]

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

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

Разделы

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

Аффилиация

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