Zulip Chat Archive
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.
Kenny Lau (May 24 2020 at 07:29):
s.nonempty
Kenny Lau (May 24 2020 at 07:30):
Bryan Gin-ge Chen said:
Yeah, you're right. PR?
Kenny Lau (May 24 2020 at 09:11):
merged
Last updated: Dec 20 2023 at 11:08 UTC