coe_eq_univ — Mathlib

English

For a finite α and a Finset s, the coercion of s to a Set is Set.univ if and only if s = univ.

Русский

Для конечного α и конечного множества s выполнено: преобразование s к множеству равно Set.univ тогда и только тогда, когда s = univ.

LaTeX

$$$(s : Set \\alpha) = \\mathrm{Set.univ} \\iff s = \\mathrm{univ}$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_univ : (s : Set α) = Set.univ ↔ s = univ := by rw [← coe_univ, coe_inj]

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