toFinset_ssubset_univ — Mathlib

English

For any s ⊆ α, the Finset corresponding to s is strictly contained in Finset.univ if and only if s is strictly contained in univ: s.toFinset ⊂ Finset.univ ↔ s ⊂ univ.

Русский

Для любого подмножества s ⊆ α верно: s.toFinset ⊂ Finset.univ ⇔ s ⊂ univ.

LaTeX

$$$s.toFinset \subsetneq \mathrm{Finset.univ} \iff s \subsetneq \mathrm{univ}$$$

Lean4

theorem toFinset_ssubset_univ [Fintype α] {s : Set α} [Fintype s] : s.toFinset ⊂ Finset.univ ↔ s ⊂ univ := by simp

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