min of non-empty set of nats

Stream: general

[Kevin Buzzard]

Presumably this is easy?

example (p : ℕ → Prop) : (∃ n : ℕ, p n) → ∃! m : ℕ, (p m ∧ ∀ d, d < m → ¬ (p d)) :=

[Kenny Lau]

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]

Thanks Kenny.