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 are associative #1300

Merged
merged 13 commits into from
Feb 14, 2025
Merged

Minimum and maximum are associative #1300

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
68ffc45
Associativity of min and max
lowasser Feb 8, 2025
4ac4f7d
Merge branch 'master' into min-max-associative
lowasser Feb 8, 2025
4a8b5c5
Formatting
lowasser Feb 8, 2025
327479d
Progress
lowasser Feb 12, 2025
3a4c279
Merge branch 'master' into min-max-associative
lowasser Feb 12, 2025
80e1863
Merge
lowasser Feb 12, 2025
6eeef9a
Fix syntax
lowasser Feb 12, 2025
eb5b231
Merge branch 'master' into min-max-associative
lowasser Feb 13, 2025
8df9c15
Merge branch 'master' into min-max-associative
lowasser Feb 13, 2025
708839f
Apply suggestions from code review
lowasser Feb 13, 2025
7a494ef
Merge remote-tracking branch 'origin/min-max-associative' into min-ma…
lowasser Feb 13, 2025
ceb5028
Follow up on review comments
lowasser Feb 13, 2025
144c52d
Fix compile
lowasser Feb 13, 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
280 changes: 200 additions & 80 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 @@ -7,6 +7,7 @@ module order-theory.decidable-total-orders where
<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.coproduct-types
open import foundation.decidable-propositions
Expand All @@ -20,7 +21,9 @@ 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.join-semilattices
open import order-theory.least-upper-bounds-posets
open import order-theory.meet-semilattices
open import order-theory.posets
open import order-theory.preorders
open import order-theory.total-orders
Expand Down Expand Up @@ -197,11 +200,11 @@ module _
where

min-Decidable-Total-Order : type-Decidable-Total-Order T
min-Decidable-Total-Order =
rec-coproduct
( λ x≤y → x)
( λ y<x → y)
( is-leq-or-strict-greater-Decidable-Total-Order T x y)
min-Decidable-Total-Order
with
is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = x
... | inr y<x = y
lowasser marked this conversation as resolved.
Show resolved Hide resolved

max-Decidable-Total-Order : type-Decidable-Total-Order T
max-Decidable-Total-Order =
Expand All @@ -211,43 +214,7 @@ module _
( is-leq-or-strict-greater-Decidable-Total-Order T x y)
```

### The minimum is a lower bound

```agda
leq-left-min-Decidable-Total-Order :
leq-Decidable-Total-Order T min-Decidable-Total-Order x
leq-left-min-Decidable-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

leq-right-min-Decidable-Total-Order :
leq-Decidable-Total-Order T min-Decidable-Total-Order y
leq-right-min-Decidable-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
```

### The maximum of two values is an upper bound

```agda
leq-left-max-Decidable-Total-Order :
leq-Decidable-Total-Order T x max-Decidable-Total-Order
leq-left-max-Decidable-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

leq-right-max-Decidable-Total-Order :
leq-Decidable-Total-Order T y max-Decidable-Total-Order
leq-right-max-Decidable-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
```

### The minimum operation is commutative
### `min x y` is the greatest lower bound of `x` and `y`
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
module _
Expand All @@ -256,44 +223,6 @@ module _
(x y : type-Decidable-Total-Order T)
where

commutative-min-Decidable-Total-Order :
min-Decidable-Total-Order T x y ＝ min-Decidable-Total-Order T y x
commutative-min-Decidable-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)))
```

### The maximum operation is commutative

```agda
commutative-max-Decidable-Total-Order :
max-Decidable-Total-Order T x y ＝ max-Decidable-Total-Order T y x
commutative-max-Decidable-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)))
```

### The minimum of two values is their greatest lower bound

```agda
min-is-greatest-binary-lower-bound-Decidable-Total-Order :
is-greatest-binary-lower-bound-Poset
( poset-Decidable-Total-Order T)
Expand Down Expand Up @@ -350,3 +279,194 @@ module _
pr2 has-least-binary-upper-bound-Decidable-Total-Order =
max-is-least-binary-upper-bound-Decidable-Total-Order
```

### `T` is a meet semilattice
lowasser marked this conversation as resolved.
Show resolved Hide resolved

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

is-meet-semilattice-Decidable-Total-Order :
is-meet-semilattice-Poset (poset-Decidable-Total-Order T)
is-meet-semilattice-Decidable-Total-Order =
has-greatest-binary-lower-bound-Decidable-Total-Order T

order-theoretic-meet-semilattice-Decidable-Total-Order :
Order-Theoretic-Meet-Semilattice l1 l2
order-theoretic-meet-semilattice-Decidable-Total-Order =
poset-Decidable-Total-Order T , is-meet-semilattice-Decidable-Total-Order
```

### `T` is a join semilattice
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
is-join-semilattice-Decidable-Total-Order :
is-join-semilattice-Poset (poset-Decidable-Total-Order T)
is-join-semilattice-Decidable-Total-Order =
has-least-binary-upper-bound-Decidable-Total-Order T

order-theoretic-join-semilattice-Decidable-Total-Order :
Order-Theoretic-Join-Semilattice l1 l2
order-theoretic-join-semilattice-Decidable-Total-Order =
poset-Decidable-Total-Order T , is-join-semilattice-Decidable-Total-Order
```

### The minimum operation is associative
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
associative-min-Decidable-Total-Order :
(x y z : type-Decidable-Total-Order T) →
min-Decidable-Total-Order T (min-Decidable-Total-Order T x y) z ＝
min-Decidable-Total-Order T x (min-Decidable-Total-Order T y z)
associative-min-Decidable-Total-Order =
associative-meet-Order-Theoretic-Meet-Semilattice
( order-theoretic-meet-semilattice-Decidable-Total-Order)
```

### The maximum operator is associative
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
associative-max-Decidable-Total-Order :
(x y z : type-Decidable-Total-Order T) →
max-Decidable-Total-Order T (max-Decidable-Total-Order T x y) z ＝
max-Decidable-Total-Order T x (max-Decidable-Total-Order T y z)
associative-max-Decidable-Total-Order =
associative-join-Order-Theoretic-Join-Semilattice
( order-theoretic-join-semilattice-Decidable-Total-Order)
```

### `min` is commutative
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
commutative-min-Decidable-Total-Order :
(x y : type-Decidable-Total-Order T) →
min-Decidable-Total-Order T x y ＝ min-Decidable-Total-Order T y x
commutative-min-Decidable-Total-Order =
commutative-meet-Order-Theoretic-Meet-Semilattice
( order-theoretic-meet-semilattice-Decidable-Total-Order)
```

### `max` is commutative
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
commutative-max-Decidable-Total-Order :
(x y : type-Decidable-Total-Order T) →
max-Decidable-Total-Order T x y ＝ max-Decidable-Total-Order T y x
commutative-max-Decidable-Total-Order =
commutative-join-Order-Theoretic-Join-Semilattice
( order-theoretic-join-semilattice-Decidable-Total-Order)
```

### `min` is idempotent
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
idempotent-min-Decidable-Total-Order :
(x : type-Decidable-Total-Order T) →
min-Decidable-Total-Order T x x ＝ x
idempotent-min-Decidable-Total-Order =
idempotent-meet-Order-Theoretic-Meet-Semilattice
( order-theoretic-meet-semilattice-Decidable-Total-Order)
```

### `max` is idempotent
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
idempotent-max-Decidable-Total-Order :
(x : type-Decidable-Total-Order T) →
max-Decidable-Total-Order T x x ＝ x
idempotent-max-Decidable-Total-Order =
idempotent-join-Order-Theoretic-Join-Semilattice
( order-theoretic-join-semilattice-Decidable-Total-Order)
```

### The minimum of two values is a lower bound
lowasser marked this conversation as resolved.
Show resolved Hide resolved

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

leq-left-min-Decidable-Total-Order :
leq-Decidable-Total-Order T (min-Decidable-Total-Order T x y) x
leq-left-min-Decidable-Total-Order =
leq-left-is-greatest-binary-lower-bound-Poset
( poset-Decidable-Total-Order T)
( min-is-greatest-binary-lower-bound-Decidable-Total-Order T x y)

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

### The maximum of two values is an upper bound

```agda
leq-left-max-Decidable-Total-Order :
leq-Decidable-Total-Order T x (max-Decidable-Total-Order T x y)
leq-left-max-Decidable-Total-Order =
leq-left-is-least-binary-upper-bound-Poset
( poset-Decidable-Total-Order T)
( max-is-least-binary-upper-bound-Decidable-Total-Order T x y)

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

### If x is less than or equal to y, the minimum of x and y is x
lowasser marked this conversation as resolved.
Show resolved Hide resolved

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

### If y is less than or equal to x, the minimum of x and y is y
lowasser marked this conversation as resolved.
Show resolved Hide resolved

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

### If x is less than or equal to y, the maximum of x and y is y
lowasser marked this conversation as resolved.
Show resolved Hide resolved

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

### If y is less than or equal to x, the maximum of x and y is x
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
right-leq-left-max-Decidable-Total-Order :
leq-Decidable-Total-Order T y x → max-Decidable-Total-Order T x y ＝ x
right-leq-left-max-Decidable-Total-Order H
with is-leq-or-strict-greater-Decidable-Total-Order T x y
... | inl x≤y = antisymmetric-leq-Decidable-Total-Order T y x H x≤y
... | inr y<x = refl
```
57 changes: 57 additions & 0 deletions src/order-theory/greatest-lower-bounds-posets.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,27 @@ module _
( is-binary-lower-bound-is-greatest-binary-lower-bound-Poset H)
```

### The greatest lower bound of a and b is the greatest lower bound of b and a
lowasser marked this conversation as resolved.
Show resolved Hide resolved

```agda
module _
{l1 l2 : Level} (P : Poset l1 l2) (a b c : type-Poset P)
where

symmetric-is-greatest-binary-lower-bound-Poset :
is-greatest-binary-lower-bound-Poset P a b c →
is-greatest-binary-lower-bound-Poset P b a c
pr1 (symmetric-is-greatest-binary-lower-bound-Poset glb-c c) glb-d =
forward-implication
( glb-c c)
( leq-right-is-binary-lower-bound-Poset P glb-d ,
leq-left-is-binary-lower-bound-Poset P glb-d)
pr1 (pr2 (symmetric-is-greatest-binary-lower-bound-Poset glb-c c) d≤c) =
leq-right-is-binary-lower-bound-Poset P (backward-implication (glb-c c) d≤c)
pr2 (pr2 (symmetric-is-greatest-binary-lower-bound-Poset glb-c c) d≤c) =
leq-left-is-binary-lower-bound-Poset P (backward-implication (glb-c c) d≤c)
```

### The proposition that two elements have a greatest lower bound

```agda
Expand Down Expand Up @@ -173,6 +194,21 @@ module _
( y , K))
```

### The property of having a greatest binary lower bound is symmetric

```agda
module _
{l1 l2 : Level} (P : Poset l1 l2) (a b : type-Poset P)
where

symmetric-has-greatest-binary-lower-bound-Poset :
has-greatest-binary-lower-bound-Poset P a b →
has-greatest-binary-lower-bound-Poset P b a
pr1 (symmetric-has-greatest-binary-lower-bound-Poset (glb , is-glb)) = glb
pr2 (symmetric-has-greatest-binary-lower-bound-Poset (glb , is-glb)) =
symmetric-is-greatest-binary-lower-bound-Poset P a b glb is-glb
```

### Greatest lower bounds of families of elements

```agda
Expand Down Expand Up @@ -291,3 +327,24 @@ module _
( x , H)
( y , K))
```

### if $a ≤ b$ then $a$ is the greatest binary lower bound of $a$ and $b$

```agda
module _
{l1 l2 : Level} (P : Poset l1 l2) (a b : type-Poset P) (p : leq-Poset P a b)
where

is-greatest-binary-lower-bound-leq-Poset :
is-greatest-binary-lower-bound-Poset P a b a
pr1 (is-greatest-binary-lower-bound-leq-Poset c) =
leq-left-is-binary-lower-bound-Poset P
pr1 (pr2 (is-greatest-binary-lower-bound-leq-Poset c) c≤a) = c≤a
pr2 (pr2 (is-greatest-binary-lower-bound-leq-Poset c) c≤a) =
transitive-leq-Poset P c a b p c≤a

has-greatest-binary-lower-bound-leq-Poset :
has-greatest-binary-lower-bound-Poset P a b
has-greatest-binary-lower-bound-leq-Poset =
( a , is-greatest-binary-lower-bound-leq-Poset)
```
Loading