mathlib docs: core.init.data.set

source

def set (α : Type u) :

Type u

Equations

set α = (α → Prop)

source

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

set α

Equations

set_of p = p

source

def set.mem {α : Type u} (a : α) (s : set α) :

Prop

Equations

set.mem a s = s a

source

@[instance]

def set.has_mem {α : Type u} :

has_mem α (set α)

Equations

set.has_mem = {mem := set.mem α}

source

def set.subset {α : Type u} (s₁ s₂ : set α) :

Prop

Equations

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

source

@[instance]

def set.has_subset {α : Type u} :

has_subset (set α)

Equations

set.has_subset = {subset := set.subset α}

source

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

set α

Equations

set.sep p s = {a : α | a ∈ s ∧ p a}

source

@[instance]

def set.has_sep {α : Type u} :

has_sep α (set α)

Equations

set.has_sep = {sep := set.sep α}

source

@[instance]

def set.has_emptyc {α : Type u} :

has_emptyc (set α)

Equations

set.has_emptyc = {emptyc := λ (a : α), false}

source

def set.univ {α : Type u} :

set α

Equations

set.univ = λ (a : α), true

source

def set.insert {α : Type u} (a : α) (s : set α) :

set α

Equations

set.insert a s = {b : α | b = a ∨ b ∈ s}

source

@[instance]

def set.has_insert {α : Type u} :

has_insert α (set α)

Equations

set.has_insert = {insert := set.insert α}

source

@[instance]

def set.has_singleton {α : Type u} :

has_singleton α (set α)

Equations

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

source

@[instance]

def set.is_lawful_singleton {α : Type u} :

is_lawful_singleton α (set α)

Equations

set.is_lawful_singleton = {insert_emptyc_eq := _}

source

def set.union {α : Type u} (s₁ s₂ : set α) :

set α

Equations

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

source

@[instance]

def set.has_union {α : Type u} :

has_union (set α)

Equations

set.has_union = {union := set.union α}

source

def set.inter {α : Type u} (s₁ s₂ : set α) :

set α

Equations

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

source

@[instance]

def set.has_inter {α : Type u} :

has_inter (set α)

Equations

set.has_inter = {inter := set.inter α}

source

def set.compl {α : Type u} (s : set α) :

set α

Equations

s.compl = {a : α | a ∉ s}

source

def set.diff {α : Type u} (s t : set α) :

set α

Equations

s.diff t = {a ∈ s | a ∉ t}

source

@[instance]

def set.has_sdiff {α : Type u} :

has_sdiff (set α)

Equations

set.has_sdiff = {sdiff := set.diff α}

source

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

set (set α)

Equations

𝒫s = {t : set α | t ⊆ s}

source

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

set α

Equations

⋃₀s = {t : α | ∃ (a : set α) (H : a ∈ s), t ∈ a}

source

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

set β

Equations

f '' s = {b : β | ∃ (a : α), a ∈ s ∧ f a = b}

source

@[instance]

def set.functor :

functor set

Equations

set.functor = {map := set.image, map_const := λ (α β : Type u_1), set.image ∘ function.const β}

source

@[instance]

def set.is_lawful_functor :

is_lawful_functor set