If I already showed that S is nonempty then it seems it should easily follow that Max S \in S but this doesn't seem to follow except when I did some toy examples like "Max{1} ∈ {1::nat}"

Let's ask the query panel what it thinks of this theorem `‹Max ?S ∈ ?S›`

```
"Max ?S ∈ ?S"
found 2 theorem(s):
Lattices_Big.linorder_class.Max_in:
finite ?A ⟹ ?A ≠ {} ⟹ Max ?A ∈ ?A
Lattices_Big.linorder_class.Max.closed:
finite ?A ⟹ ?A ≠ {} ⟹ (⋀x y. max x y ∈ {x, y}) ⟹ Max ?A ∈ ?A
```

so you need finiteness for `Max`

. Otherwise, you have to go for `Sup`

Indeed, because an infinite set might just not have a maximum, leaving `Max`

unspecified.

Last updated: Dec 07 2023 at 20:16 UTC