Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minimum and maximum for decidable total orders #1291

Merged
merged 3 commits into from
Feb 7, 2025
Merged

Minimum and maximum for decidable total orders #1291

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ebae39f
Define min and max on decidable total orders
lowasser Feb 7, 2025
c7955ae
make pre-commit
lowasser Feb 7, 2025
4919c59
Revert file
lowasser Feb 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
170 changes: 170 additions & 0 deletions src/order-theory/decidable-total-orders.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,16 @@ open import foundation.binary-relations
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.decidable-posets
open import order-theory.decidable-total-preorders
open import order-theory.greatest-lower-bounds-posets
open import order-theory.least-upper-bounds-posets
open import order-theory.posets
open import order-theory.preorders
open import order-theory.total-orders
Expand Down Expand Up @@ -181,3 +184,170 @@ module _
set-Decidable-Total-Order : Set l1
set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order
```

## Properties

### Any two elements in a decidable total order have a minimum and maximum

```agda
module _
{l1 l2 : Level}
(T : Decidable-Total-Order l1 l2)
(x y : type-Decidable-Total-Order T)
where

min-Total-Order : type-Decidable-Total-Order T
min-Total-Order =
rec-coproduct
( λ x≤y → x)
( λ y<x → y)
( is-leq-or-strict-greater-Decidable-Total-Order T x y)

max-Total-Order : type-Decidable-Total-Order T
max-Total-Order =
rec-coproduct
( λ x≤y → y)
( λ y<x → x)
( is-leq-or-strict-greater-Decidable-Total-Order T x y)
```

### `min x y ≤ x`

```agda
leq-left-min-Total-Order : leq-Decidable-Total-Order T min-Total-Order x
leq-left-min-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = refl-leq-Decidable-Total-Order T x
... | inr y<x = pr2 y<x
```

### `min x y ≤ y`

```agda
leq-right-min-Total-Order : leq-Decidable-Total-Order T min-Total-Order y
leq-right-min-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = x≤y
... | inr y<x = refl-leq-Decidable-Total-Order T y
```

### `x ≤ max x y`

```agda
leq-left-max-Total-Order : leq-Decidable-Total-Order T x max-Total-Order
leq-left-max-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = x≤y
... | inr y<x = refl-leq-Decidable-Total-Order T x
```

### `y ≤ max x y`

```agda
leq-right-max-Total-Order : leq-Decidable-Total-Order T y max-Total-Order
leq-right-max-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = refl-leq-Decidable-Total-Order T y
... | inr y<x = pr2 y<x
```

### `min` is commutative

```agda
module _
{l1 l2 : Level}
(T : Decidable-Total-Order l1 l2)
(x y : type-Decidable-Total-Order T)
where

commutative-min-Total-Order : min-Total-Order T x y ＝ min-Total-Order T y x
commutative-min-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
| is-leq-or-strict-greater-Decidable-Total-Order T y x
... | inl x≤y | inl y≤x =
antisymmetric-leq-Decidable-Total-Order T x y x≤y y≤x
... | inl x≤y | inr x<y = refl
... | inr y<x | inl y≤x = refl
... | inr y<x | inr x<y =
ex-falso
(pr1
( x<y)
( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
```

### `max` is commutative

```agda
commutative-max-Total-Order : max-Total-Order T x y ＝ max-Total-Order T y x
commutative-max-Total-Order
with is-leq-or-strict-greater-Decidable-Total-Order T x y
| is-leq-or-strict-greater-Decidable-Total-Order T y x
... | inl x≤y | inl y≤x =
antisymmetric-leq-Decidable-Total-Order T y x y≤x x≤y
... | inl x≤y | inr x<y = refl
... | inr y<x | inl y≤x = refl
... | inr y<x | inr x<y =
ex-falso
(pr1
( x<y)
( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
```

### `min x y` is the greatest lower bound of `x` and `y`

```agda
min-is-greatest-binary-lower-bound-Decidable-Total-Order :
is-greatest-binary-lower-bound-Poset
( poset-Decidable-Total-Order T)
( x)
( y)
( min-Total-Order T x y)
pr1 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) (z≤x , z≤y)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = z≤x
... | inr y<x = z≤y
pr1 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = z≤min
... | inr y<x = transitive-leq-Decidable-Total-Order T z y x (pr2 y<x) z≤min
pr2 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = transitive-leq-Decidable-Total-Order T z x y x≤y z≤min
... | inr y<x = z≤min

has-greatest-binary-lower-bound-Decidable-Total-Order :
has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y
pr1 has-greatest-binary-lower-bound-Decidable-Total-Order =
min-Total-Order T x y
pr2 has-greatest-binary-lower-bound-Decidable-Total-Order =
min-is-greatest-binary-lower-bound-Decidable-Total-Order
```

### `max x y` is the least upper bound of `x` and `y`

```agda
max-is-least-binary-upper-bound-Decidable-Total-Order :
is-least-binary-upper-bound-Poset
( poset-Decidable-Total-Order T)
( x)
( y)
( max-Total-Order T x y)
pr1 (max-is-least-binary-upper-bound-Decidable-Total-Order z) (x≤z , y≤z)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = y≤z
... | inr y<x = x≤z
pr1 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = transitive-leq-Decidable-Total-Order T x y z min≤z x≤y
... | inr y<x = min≤z
pr2 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = min≤z
... | inr y<x = transitive-leq-Decidable-Total-Order T y x z min≤z (pr2 y<x)

has-least-binary-upper-bound-Decidable-Total-Order :
has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y
pr1 has-least-binary-upper-bound-Decidable-Total-Order = max-Total-Order T x y
pr2 has-least-binary-upper-bound-Decidable-Total-Order =
max-is-least-binary-upper-bound-Decidable-Total-Order
```