Singleton_of_Element_is_Subset

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikisingleton-of-element-is-subsetsingletonssubsets

Let $S$ be a set. Let $\set x$ be the singleton of $x$ . Then $x \in S \iff \set x \subseteq S$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Singleton_of_Element_is_Subset {α : Type*} (S : Set α) (x : α) : x ∈ S ↔ {x} ⊆ S := by sorry

Source