Stream: Beginner Questions

Topic: Showing Max S is in S

Dustin Bryant (Dec 18 2022 at 23:11):

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}"

Mathias Fleury (Dec 19 2022 at 06:11):

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

Mathias Fleury (Dec 19 2022 at 06:12):

so you need finiteness for Max. Otherwise, you have to go for Sup

Wolfgang Jeltsch (Dec 19 2022 at 15:34):

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

Last updated: Apr 26 2024 at 04:17 UTC