toFinset_eq_univ

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.toFinset_eq_univ

English

For a finite s in a finite type α, h.toFinset = Finset.univ iff s = univ.

Русский

Для конечного s ⊆ α верно: h.toFinset = Finset.univ ⇔ s = univ.

LaTeX

$$$ h.toFinset = \mathrm{Finset.univ} \iff s = \mathrm{univ} $$$

Lean4

@[simp]
protected theorem toFinset_eq_univ [Fintype α] {h : s.Finite} : h.toFinset = Finset.univ ↔ s = univ :=
  @toFinset_eq_univ _ _ _ h.fintype

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

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

Разделы

Аффилиация

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