Zulip Chat Archive

Stream: general

Topic: well_founded.has_min


view this post on Zulip Kenny Lau (May 24 2020 at 07:19):

https://github.com/leanprover-community/mathlib/blob/ceb13bad567d063a3ec44d46c202dedaab25c717/src/order/basic.lean#L681-L684

/-- If `r` is a well-founded relation, then any nonempty set has a minimum element
with respect to `r`. -/
theorem has_min {α} {r : α  α  Prop} (H : well_founded r)
  (s : set α) : s.nonempty   a  s,  x  s, ¬ r x a

view this post on Zulip Kenny Lau (May 24 2020 at 07:19):

shouldn't this be a minimal element?

view this post on Zulip Bryan Gin-ge Chen (May 24 2020 at 07:22):

Yeah, you're right. PR?

view this post on Zulip Chris Hughes (May 24 2020 at 07:28):

It's only well founded, not a well order so I don't think a minimal element exists. For example the empty relation is well founded.

view this post on Zulip Kenny Lau (May 24 2020 at 07:29):

s.nonempty

view this post on Zulip Kenny Lau (May 24 2020 at 07:30):

Bryan Gin-ge Chen said:

Yeah, you're right. PR?

#2789

view this post on Zulip Kenny Lau (May 24 2020 at 09:11):

merged


Last updated: May 11 2021 at 13:22 UTC