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: Oct 12 2024 at 20:18 UTC