- SSubset : α → α → Prop
Strict subset relation:
a ⊂ b
Notation type class for the strict subset relation ⊂
.
Instances
@[inline, reducible]
Strict superset relation: a ⊃ b
Instances For
a \ b
is the set difference of a
and b
,
consisting of all elements in a
that are not in b
.
Instances For
Declare ∃ x ∈ y, ...
as syntax for ∃ x, x ∈ y ∧ ...
Instances For
Unexpander for the { x }
notation.
Instances For
Unexpander for the { x, y, ... }
notation.