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:

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) :

Equations

Set α = (α → Prop)

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

Set α

Equations

setOf p = p

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

Membership in a set

Equations

Set.Mem a s = s a

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

Set.Subset s₁ s₂ = ∀ ⦃a : α⦄, a ∈ s₁ → a ∈ s₂

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} :

HasSubset (Set α)

Equations

Set.instHasSubsetSet = { Subset := fun x x_1 => x ≤ x_1 }

instance Set.instEmptyCollectionSet {α : Type u_1} :

EmptyCollection (Set α)

Equations

Set.instEmptyCollectionSet = { emptyCollection := fun x => False }

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

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

def Set.setOf.unexpander :

Lean.PrettyPrinter.Unexpander

Equations

One or more equations did not get rendered due to their size.

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

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

def Set.univ {α : Type u_1} :

Set α

Equations

Set.univ = { _a | True }

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

Set α

Equations

Set.insert a s = { b | b = a ∨ b ∈ s }

instance Set.instInsertSet {α : Type u_1} :

Insert α (Set α)

Equations

Set.instInsertSet = { insert := Set.insert }

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

Set α

Equations

Set.singleton a = { b | b = a }

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

Set.union s₁ s₂ = { a | a ∈ s₁ ∨ a ∈ s₂ }

instance Set.instUnionSet {α : Type u_1} :

Equations

Set.instUnionSet = { union := Set.union }

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

Set α

Equations

Set.inter s₁ s₂ = { a | a ∈ s₁ ∧ a ∈ s₂ }

instance Set.instInterSet {α : Type u_1} :

Equations

Set.instInterSet = { inter := Set.inter }

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

Set α

Equations

Set.compl s = { a | ¬a ∈ s }

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

Set α

Equations

Set.diff s t = { a | a ∈ s ∧ ¬a ∈ t }

instance Set.instSDiffSet {α : Type u_1} :

Equations

Set.instSDiffSet = { sdiff := Set.diff }

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

Set (Set α)

Equations

𝒫 s = { t | t ⊆ s }

def Set.term𝒫_ :

Lean.ParserDescr

Equations

Set.term𝒫_ = Lean.ParserDescr.node `Set.term𝒫_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝒫") (Lean.ParserDescr.cat `term 100))

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

Set β

Equations

Set.image f s = { x | ∃ a, a ∈ s ∧ f a = x }

instance Set.instFunctorSet :

Equations

Set.instFunctorSet = { map := @Set.image, mapConst := fun {α β} => Set.image ∘ Function.const β }

instance Set.instLawfulFunctorSetInstFunctorSet :

LawfulFunctor Set

Equations

Set.instLawfulFunctorSetInstFunctorSet = Set.instLawfulFunctorSetInstFunctorSet.proof_1