core / init.data.set - scilib docs

source

def set (α : Type u) :

Type u

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

Equations

set α = (α → Prop)

Instances for set

source

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

set α

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

Equations

set_of p = p

Instances for ↥set_of

source

@[protected, instance]

def set.has_mem {α : Type u} :

has_mem α (set α)

Equations

set.has_mem = {mem := λ (x : α) (s : set α), s x}

source

@[simp]

theorem set.mem_set_of_eq {α : Type u} {x : α} {p : α → Prop} :

x ∈ {y : α | p y} = p x

source

@[protected, instance]

def set.has_emptyc {α : Type u} :

has_emptyc (set α)

Equations

set.has_emptyc = {emptyc := {x : α | false}}

source

def set.univ {α : Type u} :

set α

The set that contains all elements of a type.

Equations

set.univ = {x : α | true}

Instances for set.univ

set.ord_connected_univ

Instances for ↥set.univ

source

@[protected, instance]

def set.has_insert {α : Type u} :

has_insert α (set α)

Equations

set.has_insert = {insert := λ (a : α) (s : set α), {b : α | b = a ∨ b ∈ s}}

source

@[protected, instance]

def set.has_singleton {α : Type u} :

has_singleton α (set α)

Equations

set.has_singleton = {singleton := λ (a : α), {b : α | b = a}}

source

@[protected, instance]

def set.has_sep {α : Type u} :

has_sep α (set α)

Equations

set.has_sep = {sep := λ (p : α → Prop) (s : set α), {x : α | x ∈ s ∧ p x}}

source

@[protected, instance]

def set.is_lawful_singleton {α : Type u} :

is_lawful_singleton α (set α)