## Stream: general

### Topic: well_founded.has_min

#### Kenny Lau (May 24 2020 at 07:19):

/-- 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

#### Kenny Lau (May 24 2020 at 07:19):

shouldn't this be a minimal element?

#### Bryan Gin-ge Chen (May 24 2020 at 07:22):

Yeah, you're right. PR?

#### 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.

s.nonempty

#### Kenny Lau (May 24 2020 at 07:30):

Bryan Gin-ge Chen said:

Yeah, you're right. PR?

#2789

#### Kenny Lau (May 24 2020 at 09:11):

merged

Last updated: May 11 2021 at 13:22 UTC