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

Equations

• «term_⊆_» = Lean.ParserDescr.trailingNode `term_⊆_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ ") (Lean.ParserDescr.cat `term 51))

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

Equations

• «term_⊂_» = Lean.ParserDescr.trailingNode `term_⊂_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊂ ") (Lean.ParserDescr.cat `term 51))

@[inline, reducible]

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

Superset relation: a ⊇ b

Equations

• (a ⊇ b) = (b ⊆ a)

def «term_⊇_» : Lean.TrailingParserDescr

Superset relation: a ⊇ b

Equations

• «term_⊇_» = Lean.ParserDescr.trailingNode `term_⊇_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊇ ") (Lean.ParserDescr.cat `term 51))

@[inline, reducible]

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

Strict superset relation: a ⊃ b

Equations

• (a ⊃ b) = (b ⊂ a)

def «term_⊃_» : Lean.TrailingParserDescr

Strict superset relation: a ⊃ b

Equations

• «term_⊃_» = Lean.ParserDescr.trailingNode `term_⊃_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊃ ") (Lean.ParserDescr.cat `term 51))

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.

Equations

• «term_∪_» = Lean.ParserDescr.trailingNode `term_∪_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∪ ") (Lean.ParserDescr.cat `term 66))

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.

Equations

• «term_∩_» = Lean.ParserDescr.trailingNode `term_∩_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∩ ") (Lean.ParserDescr.cat `term 71))

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.

Equations

• «term_\_» = Lean.ParserDescr.trailingNode `term_\_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\ ") (Lean.ParserDescr.cat `term 71))

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 ∧ ...

Equations

• «binderTerm∈_» = Lean.ParserDescr.node `binderTerm∈_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ ") (Lean.ParserDescr.cat `term 0))

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.

Equations

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

def singletonUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the { x } notation.

Equations

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

def insertUnexpander : Lean.PrettyPrinter.Unexpander

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) [EmptyCollection β] [Insert α β] [Singleton α β] : Prop

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

  insert x ∅ = {x}

insert x ∅ = {x}