Zulip Chat Archive

Stream: general

Topic: min of non-empty set of nats


Kevin Buzzard (Jul 30 2018 at 10:49):

Presumably this is easy?

example (p :   Prop) : ( n : , p n)  ∃! m : , (p m   d, d < m  ¬ (p d)) :=

Kenny Lau (Jul 30 2018 at 10:53):

example (p :   Prop) [decidable_pred p] :
  ( n : , p n)  ∃! m : , (p m   d, d < m  ¬ (p d)) :=
λ H, nat.find H, nat.find_spec H, λ _, nat.find_min H,
λ y hy, le_antisymm (le_of_not_gt $ λ H2, hy.2 (nat.find H) H2 $ nat.find_spec H) $
nat.find_min' H hy.1

Kevin Buzzard (Jul 30 2018 at 10:55):

Thanks Kenny.


Last updated: Dec 20 2023 at 11:08 UTC