eq_singleton_iff_nonempty_unique_mem

English

Over a type with a unique element, a finset s is nonempty if and only if s = {default}.

Русский

Для типа с единственным элементом Finset s непуст тогда и только тогда, когда s = {default}.

LaTeX

$$$[Unique\,\alpha]\ s.Nonempty \iff s = \{ default \}$$$

Lean4

theorem eq_singleton_iff_nonempty_unique_mem {s : Finset α} {a : α} : s = { a } ↔ s.Nonempty ∧ ∀ x ∈ s, x = a :=
  by
  constructor
  · rintro rfl
    simp
  · rintro ⟨hne, h_uniq⟩
    rw [eq_singleton_iff_unique_mem]
    refine ⟨?_, h_uniq⟩
    rw [← h_uniq hne.choose hne.choose_spec]
    exact hne.choose_spec

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