ink

class HasSubset (α : Type u) : Type u

• Subset relation: a ⊆ b⊆ b

  Subset : α → α → Prop

Notation type class for the subset relation ⊆⊆.

ink

def «term_⊆_» : Lean.TrailingParserDescr

Subset relation: a ⊆ b⊆ b

Equations

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

ink

class HasSSubset (α : Type u) : Type u

• Strict subset relation: a ⊂ b⊂ b

  SSubset : α → α → Prop

Notation type class for the strict subset relation ⊂⊂.

ink

def «term_⊂_» : Lean.TrailingParserDescr

Strict subset relation: a ⊂ b⊂ b

Equations

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

ink

@[inline]

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

Superset relation: a ⊇ b⊇ b

Equations

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

ink

def «term_⊇_» : Lean.TrailingParserDescr

Superset relation: a ⊇ b⊇ b

Equations

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

ink

@[inline]

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

Strict superset relation: a ⊃ b⊃ b

Equations

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

ink

def «term_⊃_» : Lean.TrailingParserDescr

Strict superset relation: a ⊃ b⊃ b

Equations

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

ink

class Union (α : Type u) : Type u

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

  union : α → α → α

Notation type class for the union operation ∪∪.

ink

def «term_∪_» : Lean.TrailingParserDescr

a ∪ b∪ 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))

ink

class Inter (α : Type u) : Type u

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

  inter : α → α → α

Notation type class for the intersection operation ∩∩.

ink

def «term_∩_» : Lean.TrailingParserDescr

a ∩ b∩ 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))

ink

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

ink

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))

ink

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.

ink

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.

ink

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 }

ink

def «binderTerm∈_» : Lean.ParserDescr

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

Equations

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

ink

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.

ink

def singletonUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the { x } notation.

Equations

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

ink

def insertUnexpander : Lean.PrettyPrinter.Unexpander

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

Equations

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

ink

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

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

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

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