Skip to content

Commit 32ba99d

Browse files
lowasserlowasser
authored
Poset of closed intervals (#1563)
Closed intervals in a poset (or total order) themselves form a poset.
1 parent 90edd94 commit 32ba99d

11 files changed

+798
-4
lines changed

‎src/elementary-number-theory.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,7 @@ open import elementary-number-theory.initial-segments-natural-numbers public
107107
open import elementary-number-theory.integer-fractions public
108108
open import elementary-number-theory.integer-partitions public
109109
open import elementary-number-theory.integers public
110+
open import elementary-number-theory.intersections-closed-intervals-rational-numbers public
110111
open import elementary-number-theory.jacobi-symbol public
111112
open import elementary-number-theory.kolakoski-sequence public
112113
open import elementary-number-theory.legendre-symbol public
@@ -157,6 +158,7 @@ open import elementary-number-theory.ordinal-induction-natural-numbers public
157158
open import elementary-number-theory.parity-natural-numbers public
158159
open import elementary-number-theory.peano-arithmetic public
159160
open import elementary-number-theory.pisano-periods public
161+
open import elementary-number-theory.poset-closed-intervals-rational-numbers public
160162
open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public
161163
open import elementary-number-theory.positive-and-negative-integers public
162164
open import elementary-number-theory.positive-and-negative-rational-numbers public

‎src/elementary-number-theory/intersections-closed-intervals-rational-numbers.lagda.md‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
# Intersections of closed intervals of rational numbers
2+
3+
```agda
4+
module elementary-number-theory.intersections-closed-intervals-rational-numbers where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.closed-intervals-rational-numbers
11+
open import elementary-number-theory.decidable-total-order-rational-numbers
12+
open import elementary-number-theory.poset-closed-intervals-rational-numbers
13+
14+
open import foundation.binary-relations
15+
open import foundation.identity-types
16+
open import foundation.intersections-subtypes
17+
open import foundation.universe-levels
18+
19+
open import order-theory.greatest-lower-bounds-posets
20+
open import order-theory.intersections-closed-intervals-total-orders
21+
```
22+
23+
</details>
24+
25+
## Idea
26+
27+
Two
28+
[closed intervals](elementary-number-theory.closed-intervals-rational-numbers.md)
29+
[a, b] and [c, d] of
30+
[rational numbers](elementary-number-theory.rational-numbers.md)
31+
{{#concept "intersect" Disambiguation="closed intervals of rational numbers"}}
32+
if `a ≤ d` and `c ≤ b`.
33+
34+
If [a, b] and [c, d] intersect, their intersection is itself a closed interval.
35+
36+
## Definition
37+
38+
```agda
39+
intersect-prop-closed-interval-ℚ : Relation-Prop lzero closed-interval-ℚ
40+
intersect-prop-closed-interval-ℚ =
41+
intersect-prop-closed-interval-Total-Order ℚ-Total-Order
42+
43+
intersect-closed-interval-ℚ : Relation lzero closed-interval-ℚ
44+
intersect-closed-interval-ℚ =
45+
intersect-closed-interval-Total-Order ℚ-Total-Order
46+
```
47+
48+
## Properties
49+
50+
### Intersection is reflexive
51+
52+
```agda
53+
refl-intersect-closed-interval-ℚ : is-reflexive intersect-closed-interval-ℚ
54+
refl-intersect-closed-interval-ℚ =
55+
refl-intersect-closed-interval-Total-Order ℚ-Total-Order
56+
```
57+
58+
### If two intervals intersect, their intersection is a closed interval
59+
60+
```agda
61+
intersection-closed-interval-ℚ :
62+
([a,b] [c,d] : closed-interval-ℚ) → intersect-closed-interval-ℚ [a,b] [c,d] →
63+
closed-interval-ℚ
64+
intersection-closed-interval-ℚ =
65+
intersection-closed-interval-Total-Order ℚ-Total-Order
66+
67+
is-intersection-closed-interval-ℚ :
68+
([a,b] [c,d] : closed-interval-ℚ) →
69+
(H : intersect-closed-interval-ℚ [a,b] [c,d]) →
70+
subtype-closed-interval-ℚ
71+
( intersection-closed-interval-ℚ [a,b] [c,d] H) ＝
72+
intersection-subtype
73+
( subtype-closed-interval-ℚ [a,b])
74+
( subtype-closed-interval-ℚ [c,d])
75+
is-intersection-closed-interval-ℚ =
76+
is-intersection-closed-interval-Total-Order ℚ-Total-Order
77+
78+
intersect-closed-interval-intersect-subtype-ℚ :
79+
([a,b] [c,d] : closed-interval-ℚ) →
80+
intersect-subtype
81+
( subtype-closed-interval-ℚ [a,b])
82+
( subtype-closed-interval-ℚ [c,d]) →
83+
intersect-closed-interval-ℚ [a,b] [c,d]
84+
intersect-closed-interval-intersect-subtype-ℚ =
85+
intersect-closed-interval-intersect-subtype-Total-Order ℚ-Total-Order
86+
```
87+
88+
### If two closed intervals intersect, their intersection is their greatest lower bound
89+
90+
```agda
91+
is-greatest-binary-lower-bound-intersection-closed-interval-ℚ :
92+
([a,b] [c,d] : closed-interval-ℚ) →
93+
(H : intersect-closed-interval-ℚ [a,b] [c,d]) →
94+
is-greatest-binary-lower-bound-Poset
95+
( poset-closed-interval-ℚ)
96+
( [a,b])
97+
( [c,d])
98+
( intersection-closed-interval-ℚ [a,b] [c,d] H)
99+
is-greatest-binary-lower-bound-intersection-closed-interval-ℚ =
100+
is-greatest-binary-lower-bound-intersection-closed-interval-Total-Order
101+
( ℚ-Total-Order)
102+
```
103+
104+
### If two closed intervals intersect, their intersection is contained in both
105+
106+
```agda
107+
abstract
108+
leq-left-intersection-closed-interval-ℚ :
109+
([a,b] [c,d] : closed-interval-ℚ) →
110+
(H : intersect-closed-interval-ℚ [a,b] [c,d]) →
111+
leq-closed-interval-ℚ (intersection-closed-interval-ℚ [a,b] [c,d] H) [a,b]
112+
leq-left-intersection-closed-interval-ℚ =
113+
leq-left-intersection-closed-interval-Total-Order ℚ-Total-Order
114+
115+
leq-right-intersection-closed-interval-ℚ :
116+
([a,b] [c,d] : closed-interval-ℚ) →
117+
(H : intersect-closed-interval-ℚ [a,b] [c,d]) →
118+
leq-closed-interval-ℚ (intersection-closed-interval-ℚ [a,b] [c,d] H) [c,d]
119+
leq-right-intersection-closed-interval-ℚ =
120+
leq-right-intersection-closed-interval-Total-Order ℚ-Total-Order
121+
```

‎src/elementary-number-theory/poset-closed-intervals-rational-numbers.lagda.md‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
# The poset of closed intervals of rational numbers
2+
3+
```agda
4+
module elementary-number-theory.poset-closed-intervals-rational-numbers where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.closed-intervals-rational-numbers
11+
open import elementary-number-theory.decidable-total-order-rational-numbers
12+
13+
open import foundation.binary-relations
14+
open import foundation.universe-levels
15+
16+
open import order-theory.closed-intervals-total-orders
17+
open import order-theory.poset-closed-intervals-total-orders
18+
open import order-theory.posets
19+
open import order-theory.preorders
20+
```
21+
22+
</details>
23+
24+
## Idea
25+
26+
The
27+
[closed intervals](elementary-number-theory.closed-intervals-rational-numbers.md)
28+
of [rational numbers](elementary-number-theory.rational-numbers.md) form a
29+
[poset](order-theory.posets.md) under the containment relation.
30+
31+
## Definition
32+
33+
```agda
34+
leq-prop-closed-interval-ℚ : Relation-Prop lzero closed-interval-ℚ
35+
leq-prop-closed-interval-ℚ =
36+
leq-prop-closed-interval-Total-Order ℚ-Total-Order
37+
38+
leq-closed-interval-ℚ : Relation lzero closed-interval-ℚ
39+
leq-closed-interval-ℚ = leq-closed-interval-Total-Order ℚ-Total-Order
40+
```
41+
42+
## Properties
43+
44+
### The containment relation is a partial order
45+
46+
```agda
47+
abstract
48+
refl-leq-closed-interval-ℚ : is-reflexive leq-closed-interval-ℚ
49+
refl-leq-closed-interval-ℚ =
50+
refl-leq-closed-interval-Total-Order ℚ-Total-Order
51+
52+
transitive-leq-closed-interval-ℚ : is-transitive leq-closed-interval-ℚ
53+
transitive-leq-closed-interval-ℚ =
54+
transitive-leq-closed-interval-Total-Order ℚ-Total-Order
55+
56+
antisymmetric-leq-closed-interval-ℚ : is-antisymmetric leq-closed-interval-ℚ
57+
antisymmetric-leq-closed-interval-ℚ =
58+
antisymmetric-leq-closed-interval-Total-Order ℚ-Total-Order
59+
60+
poset-closed-interval-ℚ : Poset lzero lzero
61+
poset-closed-interval-ℚ = poset-closed-interval-Total-Order ℚ-Total-Order
62+
```

‎src/order-theory.lagda.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ open import order-theory.inflattices public
6363
open import order-theory.inhabited-chains-posets public
6464
open import order-theory.inhabited-chains-preorders public
6565
open import order-theory.inhabited-finite-total-orders public
66+
open import order-theory.intersections-closed-intervals-total-orders public
6667
open import order-theory.interval-subposets public
6768
open import order-theory.join-preserving-maps-posets public
6869
open import order-theory.join-semilattices public
@@ -108,6 +109,8 @@ open import order-theory.order-preserving-maps-large-preorders public
108109
open import order-theory.order-preserving-maps-posets public
109110
open import order-theory.order-preserving-maps-preorders public
110111
open import order-theory.ordinals public
112+
open import order-theory.poset-closed-intervals-posets public
113+
open import order-theory.poset-closed-intervals-total-orders public
111114
open import order-theory.posets public
112115
open import order-theory.powers-of-large-locales public
113116
open import order-theory.precategory-of-decidable-total-orders public
@@ -134,6 +137,7 @@ open import order-theory.similarity-of-elements-strict-orders public
134137
open import order-theory.similarity-of-elements-strict-preorders public
135138
open import order-theory.similarity-of-order-preserving-maps-large-posets public
136139
open import order-theory.similarity-of-order-preserving-maps-large-preorders public
140+
open import order-theory.spans-closed-intervals-total-orders public
137141
open import order-theory.strict-order-preserving-maps public
138142
open import order-theory.strict-orders public
139143
open import order-theory.strict-preorders public

0 commit comments

Comments
 (0)