Minimum and maximum are associative

[lowasser]

If anyone has any ideas on how to do this without a ton of casework, I'd love to hear it.

[fredrik-bakke]

Associativity should follow from uniqueness of greatest binary lower/upper bounds. I.e., this is a property of binary meets/joins in arbitrary posets. It's probably easier to start there, if it hasn't been formalized already.

[fredrik-bakke]

It hasn't been formalized yet, but an argument sketch that should be straightforward given the proper infrastructure is as follows:

1. The left associated twice iterated minimum is the greatest lower bound of the appropriate family on the three-element set.
2. The right associated twice iterated minimum is the greatest lower bound of the same family on the three-element set.
3. By essential uniqueness, the two elements are similar, already in an arbitrary preorder.
4. By antisymmetry in a poset, the two elements are equal.

[EgbertRijke]

I agree with Fredrik, this shouldn't be formalized by case analysis, but it should be formalized at the level of meets and joins in meet-semilattices and join-semilattices.

[lowasser]

I think it already is, e.g. here. I will try to reuse that.

[fredrik-bakke]

I think it already is, e.g. here. I will try to reuse that.

Excellent!

[lowasser]

All right, we should be good to go.

[fredrik-bakke]

Great work! Merging now