mathlib documentation

core.init.data.set

def set  :
Type uType u

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

Equations
def set.mem {α : Type u} :
α → set α → Prop

Equations
@[instance]
def set.has_mem {α : Type u} :
has_mem α (set α)

Equations
def set.subset {α : Type u} :
set αset α → Prop

Equations
@[instance]
def set.has_subset {α : Type u} :

Equations
def set.sep {α : Type u} :
(α → Prop)set αset α

Equations
@[instance]
def set.has_sep {α : Type u} :
has_sep α (set α)

Equations
@[instance]
def set.has_emptyc {α : Type u} :

Equations
def set.univ {α : Type u} :
set α

Equations
def set.insert {α : Type u} :
α → set αset α

Equations
@[instance]
def set.has_insert {α : Type u} :
has_insert α (set α)

Equations
@[instance]
def set.has_singleton {α : Type u} :

Equations
@[instance]
def set.is_lawful_singleton {α : Type u} :

Equations
def set.union {α : Type u} :
set αset αset α

Equations
@[instance]
def set.has_union {α : Type u} :

Equations
def set.inter {α : Type u} :
set αset αset α

Equations
@[instance]
def set.has_inter {α : Type u} :

Equations
def set.compl {α : Type u} :
set αset α

Equations
def set.diff {α : Type u} :
set αset αset α

Equations
@[instance]
def set.has_sdiff {α : Type u} :

Equations
def set.powerset {α : Type u} :
set αset (set α)

Equations
def set.sUnion {α : Type u} :
set (set α)set α

Equations
def set.image {α : Type u} {β : Type v} :
(α → β)set αset β

Equations
  • f '' s = {b : β | ∃ (a : α), a s f a = b}
@[instance]

Equations