Intervals as multisets #
This file defines intervals as multisets.
Main declarations #
In a LocallyFiniteOrder
,
Multiset.Icc
: Closed-closed interval as a multiset.Multiset.Ico
: Closed-open interval as a multiset.Multiset.Ioc
: Open-closed interval as a multiset.Multiset.Ioo
: Open-open interval as a multiset.
In a LocallyFiniteOrderTop
,
Multiset.Ici
: Closed-infinite interval as a multiset.Multiset.Ioi
: Open-infinite interval as a multiset.
In a LocallyFiniteOrderBot
,
Multiset.Iic
: Infinite-open interval as a multiset.Multiset.Iio
: Infinite-closed interval as a multiset.
TODO #
Do we really need this file at all? (March 2024)
The multiset of elements x
such that a ≤ x
and x ≤ b
. Basically Set.Icc a b
as a
multiset.
Instances For
The multiset of elements x
such that a ≤ x
and x < b
. Basically Set.Ico a b
as a
multiset.
Instances For
The multiset of elements x
such that a < x
and x ≤ b
. Basically Set.Ioc a b
as a
multiset.
Instances For
The multiset of elements x
such that a < x
and x < b
. Basically Set.Ioo a b
as a
multiset.
Instances For
The multiset of elements x
such that a ≤ x
. Basically Set.Ici a
as a multiset.
Instances For
The multiset of elements x
such that a < x
. Basically Set.Ioi a
as a multiset.
Instances For
The multiset of elements x
such that x ≤ b
. Basically Set.Iic b
as a multiset.
Instances For
The multiset of elements x
such that x < b
. Basically Set.Iio b
as a multiset.
Instances For
Alias of the reverse direction of Multiset.Icc_eq_zero_iff
.
Alias of the reverse direction of Multiset.Ico_eq_zero_iff
.
Alias of the reverse direction of Multiset.Ioc_eq_zero_iff
.