# Documentation

Std.Classes.SetNotation

class HasSubset (α : Type u) :
• Subset relation: a ⊆ b⊆ b

Subset : ααProp

Notation type class for the subset relation ⊆⊆.

Instances

Subset relation: a ⊆ b⊆ b

Equations
class HasSSubset (α : Type u) :
• Strict subset relation: a ⊂ b⊂ b

SSubset : ααProp

Notation type class for the strict subset relation ⊂⊂.

Instances

Strict subset relation: a ⊂ b⊂ b

Equations
@[inline]
abbrev Superset {α : Type u_1} [inst : ] (a : α) (b : α) :

Superset relation: a ⊇ b⊇ b

Equations

Superset relation: a ⊇ b⊇ b

Equations
@[inline]
abbrev SSuperset {α : Type u_1} [inst : ] (a : α) (b : α) :

Strict superset relation: a ⊃ b⊃ b

Equations

Strict superset relation: a ⊃ b⊃ b

Equations
class Union (α : Type u) :
• a ∪ b∪ b is the union ofa and b.

union : ααα

Notation type class for the union operation ∪∪.

Instances

a ∪ b∪ b is the union ofa and b.

Equations
class Inter (α : Type u) :
• a ∩ b∩ b is the intersection ofa and b.

inter : ααα

Notation type class for the intersection operation ∩∩.

Instances

a ∩ b∩ b is the intersection ofa and b.

Equations
class SDiff (α : Type u) :
• a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

sdiff : ααα

Notation type class for the set difference \.

Instances

a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

Equations
class Insert (α : outParam (Type u)) (γ : Type v) :
Type (maxuv)
• insert x xs inserts the element x into the collection xs.

insert : αγγ

Type class for the insert operation. Used to implement the { a, b, c } syntax.

Instances
class Singleton (α : outParam (Type u)) (β : Type v) :
Type (maxuv)
• singleton x is a collection with the single element x (notation: {x}).

singleton : αβ

Type class for the singleton operation. Used to implement the { a, b, c } syntax.

Instances
class Sep (α : outParam (Type u)) (γ : Type v) :
Type (maxuv)
• Computes { a ∈ c | p a }∈ c | p a }.

sep : (αProp) → γγ

Type class used to implement the notation { a ∈ c | p a }∈ c | p a }

Instances

Declare ∃ x ∈ y, ...∃ x ∈ y, ...∈ y, ... as syntax for ∃ x, x ∈ y ∧ ...∃ x, x ∈ y ∧ ...∈ y ∧ ...∧ ...

Equations

{ a, b, c } is a set with elements a, b, and c.

This notation works for all types that implement Insert and Singleton.

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

Unexpander for the { x } notation.

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

Unexpander for the { x, y, ... } notation.

Equations
• One or more equations did not get rendered due to their size.
class IsLawfulSingleton (α : Type u) (β : Type v) [inst : ] [inst : Insert α β] [inst : ] :
• insert x ∅ = {x}∅ = {x}

insert_emptyc_eq : ∀ (x : α), = {x}

insert x ∅ = {x}∅ = {x}

Instances