eq_univ — Mathlib

English

If α is a subsingleton, every nonempty Finset s equals univ.

Русский

Если α является подмножество с одним элементом, любой непустой Finset s равен univ.

LaTeX

$$$ [Subsingleton \\alpha] \\\\Rightarrow \\\\forall s : \\\\mathrm{Finset} \\\\alpha, s \\\\mathrm{Nonempty} \\\\Rightarrow s = \\\\mathrm{univ}$$$

Lean4

theorem eq_univ [Subsingleton α] : s.Nonempty → s = univ :=
  by
  rintro ⟨x, hx⟩
  exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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