class HasSubset (α : Type u) : Type u

• Subset : α → α → Prop

  Subset relation: a ⊆ b

Notation type class for the subset relation ⊆.

def «term_⊆_» : Lean.TrailingParserDescr

Subset relation: a ⊆ b

class HasSSubset (α : Type u) : Type u

• SSubset : α → α → Prop

  Strict subset relation: a ⊂ b

Notation type class for the strict subset relation ⊂.

def «term_⊂_» : Lean.TrailingParserDescr

Strict subset relation: a ⊂ b

@[inline, reducible]

abbrev Superset {α : Type u_1} [HasSubset α] (a : α) (b : α) : Prop

Superset relation: a ⊇ b

def «term_⊇_» : Lean.TrailingParserDescr

Superset relation: a ⊇ b

@[inline, reducible]

abbrev SSuperset {α : Type u_1} [HasSSubset α] (a : α) (b : α) : Prop

Strict superset relation: a ⊃ b

def «term_⊃_» : Lean.TrailingParserDescr

Strict superset relation: a ⊃ b

class Union (α : Type u) : Type u

• union : α → α → α

  a ∪ b is the union ofa and b.

Notation type class for the union operation ∪.

def «term_∪_» : Lean.TrailingParserDescr

a ∪ b is the union ofa and b.

class Inter (α : Type u) : Type u

• inter : α → α → α

  a ∩ b is the intersection ofa and b.

Notation type class for the intersection operation ∩.

def «term_∩_» : Lean.TrailingParserDescr

a ∩ b is the intersection ofa and b.

class SDiff (α : Type u) : 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 \.

def «term_\_» : Lean.TrailingParserDescr

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

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.

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.

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 }

def «binderTerm∈_» : Lean.ParserDescr

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

def «term{_}» : Lean.ParserDescr

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

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

def singletonUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the { x } notation.

def insertUnexpander : Lean.PrettyPrinter.Unexpander

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

class IsLawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] : Prop

• insert_emptyc_eq : ∀ (x : α), insert x ∅ = {x}

  insert x ∅ = {x}

insert x ∅ = {x}