toFinset_eq_univ — Mathlib

English

Let α be a finite type and s a subset of α. Then s equals the entire universe if and only if its finite representation is the universal finite set: s = univ ⇔ s.toFinset = Finset.univ.

Русский

Пусть α — конечный тип, s — подмножество α. Тогда s равно всего множества тогда и только тогда, когда его конечное представление равно универсальному конечному множеству: s = univ ⇔ s.toFinset = Finset.univ.

LaTeX

$$$s = \mathrm{univ} \;\Longleftrightarrow\; s.toFinset = \mathrm{Finset.univ}$$$

Lean4

@[simp]
theorem toFinset_eq_univ [Fintype α] [Fintype s] : s.toFinset = Finset.univ ↔ s = univ := by
  rw [← coe_inj, coe_toFinset, coe_univ]

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