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))
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))
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))
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))
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))
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))
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))
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))
Unexpander for the { x }
notation.
Equations
- One or more equations did not get rendered due to their size.
Unexpander for the { x, y, ... }
notation.
Equations
- One or more equations did not get rendered due to their size.