Sets

This file sets up the theory of sets whose elements have a given type.

Main definitions

Given a type X and a predicate p : X → Prop:

• Set X : the type of sets whose elements have type X
• {a : X | p a} : Set X : the set of all elements of X satisfying p
• {a | p a} : Set X : a more concise notation for {a : X | p a}
• {a ∈ S | p a} : Set X : given S : Set X, the subset of S consisting of its elements satisfying p.

Implementation issues

As in Lean 3, Set X := X → Prop

I didn't call this file Data.Set.Basic because it contains core Lean 3 stuff which happens before mathlib3's data.set.basic . This file is a port of the core Lean 3 file lib/lean/library/init/data/set.lean.

def Set (α : Type u) : Type u

def setOf {α : Type u} (p : α → Prop) : Set α

def Set.Mem {α : Type u_1} (a : α) (s : Set α) : Prop

Membership in a set

instance Set.instMembershipSet {α : Type u_1} : Membership α (Set α)

theorem Set.ext {α : Type u_1} {a : Set α} {b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b

def Set.Subset {α : Type u_1} (s₁ : Set α) (s₂ : Set α) : Prop

instance Set.instLESet {α : Type u_1} : LE (Set α)

Porting note: we introduce ≤ before ⊆ to help the unifier when applying lattice theorems to subset hypotheses.

instance Set.instHasSubsetSet {α : Type u_1} : HasSubset (Set α)

instance Set.instEmptyCollectionSet {α : Type u_1} : EmptyCollection (Set α)

def Set.«term{_|_}» : Lean.ParserDescr

def Set.setOf.unexpander : Lean.PrettyPrinter.Unexpander

def Set.«term{_|_}_1» : Lean.ParserDescr

def Set.univ {α : Type u_1} : Set α

def Set.insert {α : Type u_1} (a : α) (s : Set α) : Set α

instance Set.instInsertSet {α : Type u_1} : Insert α (Set α)

def Set.singleton {α : Type u_1} (a : α) : Set α

instance Set.instSingletonSet {α : Type u_1} : Singleton α (Set α)

def Set.union {α : Type u_1} (s₁ : Set α) (s₂ : Set α) : Set α

instance Set.instUnionSet {α : Type u_1} : Union (Set α)

def Set.inter {α : Type u_1} (s₁ : Set α) (s₂ : Set α) : Set α

instance Set.instInterSet {α : Type u_1} : Inter (Set α)

def Set.compl {α : Type u_1} (s : Set α) : Set α

def Set.diff {α : Type u_1} (s : Set α) (t : Set α) : Set α

instance Set.instSDiffSet {α : Type u_1} : SDiff (Set α)

def Set.powerset {α : Type u_1} (s : Set α) : Set (Set α)

def Set.term𝒫_ : Lean.ParserDescr

def Set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set β

instance Set.instFunctorSet : Functor Set

instance Set.instLawfulFunctorSetInstFunctorSet : LawfulFunctor Set