Stream: Beginner Questions

Topic: Showing Max S is in S


view this post on Zulip 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}"

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Dec 19 2022 at 06:12):

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

view this post on Zulip Wolfgang Jeltsch (Dec 19 2022 at 15:34):

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


Last updated: Feb 27 2024 at 08:17 UTC