mathlib documentation

core / init.data.set

def set (α : Type u) :
Type u

A set of elements of type α; implemented as a predicate α → Prop.

Equations
  • set α = (α → Prop)
Instances for set
def set_of {α : Type u} (p : α → Prop) :
set α

The set {x | p x} of elements satisfying the predicate p.

Equations
Instances for set_of
@[protected, instance]
def set.has_mem {α : Type u} :
has_mem α (set α)
Equations
@[simp]
theorem set.mem_set_of_eq {α : Type u} {x : α} {p : α → Prop} :
x {y : α | p y} = p x
@[protected, instance]
def set.has_emptyc {α : Type u} :
Equations
def set.univ {α : Type u} :
set α

The set that contains all elements of a type.

Equations
Instances for set.univ
Instances for set.univ
@[protected, instance]
def set.has_insert {α : Type u} :
has_insert α (set α)
Equations
@[protected, instance]
def set.has_singleton {α : Type u} :
Equations
@[protected, instance]
def set.has_sep {α : Type u} :
has_sep α (set α)
Equations
@[protected, instance]
def set.is_lawful_singleton {α : Type u} :