Documentation

Mathlib.Init.Set

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:

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) :
Equations
def setOf {α : Type u} (p : αProp) :
Set α
Equations
def Set.Mem {α : Type u_1} (a : α) (s : Set α) :

Membership in a set

Equations
instance Set.instMembershipSet {α : Type u_1} :
Membership α (Set α)
Equations
  • Set.instMembershipSet = { mem := Set.Mem }
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 α) :
Equations
instance Set.instLESet {α : Type u_1} :
LE (Set α)

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

Equations
  • Set.instLESet = { le := Set.Subset }
instance Set.instHasSubsetSet {α : Type u_1} :
Equations
  • Set.instHasSubsetSet = { Subset := fun x x_1 => x x_1 }
Equations
  • Set.instEmptyCollectionSet = { emptyCollection := fun x => False }
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Set.univ {α : Type u_1} :
Set α
Equations
def Set.insert {α : Type u_1} (a : α) (s : Set α) :
Set α
Equations
instance Set.instInsertSet {α : Type u_1} :
Insert α (Set α)
Equations
  • Set.instInsertSet = { insert := Set.insert }
def Set.singleton {α : Type u_1} (a : α) :
Set α
Equations
instance Set.instSingletonSet {α : Type u_1} :
Singleton α (Set α)
Equations
  • Set.instSingletonSet = { singleton := Set.singleton }
def Set.union {α : Type u_1} (s₁ : Set α) (s₂ : Set α) :
Set α
Equations
instance Set.instUnionSet {α : Type u_1} :
Union (Set α)
Equations
  • Set.instUnionSet = { union := Set.union }
def Set.inter {α : Type u_1} (s₁ : Set α) (s₂ : Set α) :
Set α
Equations
instance Set.instInterSet {α : Type u_1} :
Inter (Set α)
Equations
  • Set.instInterSet = { inter := Set.inter }
def Set.compl {α : Type u_1} (s : Set α) :
Set α
Equations
def Set.diff {α : Type u_1} (s : Set α) (t : Set α) :
Set α
Equations
instance Set.instSDiffSet {α : Type u_1} :
SDiff (Set α)
Equations
  • Set.instSDiffSet = { sdiff := Set.diff }
def Set.powerset {α : Type u_1} (s : Set α) :
Set (Set α)
Equations
def Set.image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
Set β
Equations
Equations