Intervals #
In any preorder α
, we define intervals
(which on each side can be either infinite, open, or closed) using the following naming conventions:
i
: infiniteo
: openc
: closed
Each interval has the name I
+ letter for left side + letter for right side.
For instance, Ioc a b
denotes the interval (a, b]
.
The definitions can be found in Order/Interval/Set/Defs
.
This file contains basic facts on inclusion, intersection, difference of intervals
(where the precise statements may depend on the properties of the order,
in particular for some statements it should be LinearOrder
or DenselyOrdered
).
TODO: This is just the beginning; a lot of rules are missing
In an order without maximal elements, the intervals Ioi
are nonempty.
Equations
- ⋯ = ⋯
In an order without minimal elements, the intervals Iio
are nonempty.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of the reverse direction of Set.Ici_subset_Ici
.
Alias of the reverse direction of Set.Iic_subset_Iic
.
If a ≤ b
, then (b, +∞) ⊆ (a, +∞)
. In preorders, this is just an implication. If you need
the equivalence in linear orders, use Ioi_subset_Ioi_iff
.
If a ≤ b
, then (b, +∞) ⊆ [a, +∞)
. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use Ioi_subset_Ici_iff
.
If a ≤ b
, then (-∞, a) ⊆ (-∞, b)
. In preorders, this is just an implication. If you need
the equivalence in linear orders, use Iio_subset_Iio_iff
.
If a ≤ b
, then (-∞, a) ⊆ (-∞, b]
. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use Iio_subset_Iic_iff
.
Alias of the reverse direction of Set.Ioi_eq_empty_iff
.
Alias of the reverse direction of Set.Iio_eq_empty_iff
.
Equations
- Set.instIccUnique = { default := ⟨a, ⋯⟩, uniq := ⋯ }
Unions of adjacent intervals #
Two infinite intervals #
A finite and an infinite interval #
An infinite and a finite interval #
Two finite intervals, I?o
and Ic?
#
Two finite intervals, I?c
and Io?
#
Two finite intervals with a common point #
Closed intervals in α × β
#
Lemmas about intervals in dense orders #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯