class HasSubset (α : Type u) : Type u

Notation type class for the subset relation ⊆.

• Subset : α → α → Prop

  Subset relation: a ⊆ b

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

Notation type class for the strict subset relation ⊂.

• SSubset : α → α → Prop

  Strict subset relation: a ⊂ b

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

Notation type class for the union operation ∪.

• union : α → α → α

  a ∪ b is the union ofa and b.

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

Notation type class for the intersection operation ∩.

• inter : α → α → α

  a ∩ b is the intersection ofa and b.

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

Notation type class for the set difference \.

• sdiff : α → α → α

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

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)

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

• insert : α → γ → γ

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

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

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

• singleton : α → β

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

class Sep (α : outParam (Type u)) (γ : Type v) : Type (max u v)

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

• sep : (α → Prop) → γ → γ

  Computes { a ∈ c | p a }.

def «binderTerm∈_» : Lean.ParserDescr

Declare ∀ x ∈ y, ... as syntax for ∀ x, x ∈ y → ... and ∃ 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 «binderTerm∉_» : Lean.ParserDescr

Declare ∀ x ∉ y, ... as syntax for ∀ x, x ∉ y → ... and ∃ 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 «binderTerm⊆_» : Lean.ParserDescr

Declare ∀ x ⊆ y, ... as syntax for ∀ x, x ⊆ y → ... and ∃ 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 «binderTerm⊂_» : Lean.ParserDescr

Declare ∀ x ⊂ y, ... as syntax for ∀ x, x ⊂ y → ... and ∃ 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 «binderTerm⊇_» : Lean.ParserDescr

Declare ∀ x ⊇ y, ... as syntax for ∀ x, x ⊇ y → ... and ∃ 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 «binderTerm⊃_» : Lean.ParserDescr

Declare ∀ x ⊃ y, ... as syntax for ∀ x, x ⊃ y → ... and ∃ 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 x ∅ = {x}

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

  insert x ∅ = {x}