subsingleton_iff_exists_singleton_mem

English

If α is nonempty, then l is subsingleton iff there exists a such that {a} ∈ l.

Русский

Если α непусто, то l подсинглетен тогда и только тогда, когда существует a такой, что {a} ∈ l.

LaTeX

$$$$ [Nonempty α] : l.Subsingleton \iff ∃ a, {a} \in l $$$$

Lean4

theorem subsingleton_iff_exists_singleton_mem [Nonempty α] : l.Subsingleton ↔ ∃ a, { a } ∈ l := by
  simp only [subsingleton_iff_exists_le_pure, le_pure_iff]

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