# Documentation

Std.Classes.SetNotation

class HasSubset (α : Type u) :
• Subset : ααProp

Subset relation: a ⊆ b

Notation type class for the subset relation ⊆.

Instances

Subset relation: a ⊆ b

Instances For
class HasSSubset (α : Type u) :
• SSubset : ααProp

Strict subset relation: a ⊂ b

Notation type class for the strict subset relation ⊂.

Instances

Strict subset relation: a ⊂ b

Instances For
@[inline, reducible]
abbrev Superset {α : Type u_1} [] (a : α) (b : α) :

Superset relation: a ⊇ b

Instances For

Superset relation: a ⊇ b

Instances For
@[inline, reducible]
abbrev SSuperset {α : Type u_1} [] (a : α) (b : α) :

Strict superset relation: a ⊃ b

Instances For

Strict superset relation: a ⊃ b

Instances For
class Union (α : Type u) :
• union : ααα

a ∪ b is the union ofa and b.

Notation type class for the union operation ∪.

Instances

a ∪ b is the union ofa and b.

Instances For
class Inter (α : Type u) :
• inter : ααα

a ∩ b is the intersection ofa and b.

Notation type class for the intersection operation ∩.

Instances

a ∩ b is the intersection ofa and b.

Instances For
class SDiff (α : Type u) :
• sdiff : ααα

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

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.

Instances For
class Insert (α : outParam (Type u)) (γ : Type v) :
Type (max u v)
• insert : αγγ

insert x xs inserts the element x into the collection xs.

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

Instances
class Singleton (α : outParam (Type u)) (β : Type v) :
Type (max u v)
• singleton : αβ

singleton x is a collection with the single element x (notation: {x}).

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

Instances
class Sep (α : outParam (Type u)) (γ : Type v) :
Type (max u v)
• sep : (αProp) → γγ

Computes { a ∈ c | p a }.

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

Instances

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

Instances For

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

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

Instances For

Unexpander for the { x } notation.

Instances For

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

Instances For
class IsLawfulSingleton (α : Type u) (β : Type v) [] [Insert α β] [] :
• insert_emptyc_eq : ∀ (x : α), = {x}

insert x ∅ = {x}

insert x ∅ = {x}

Instances