Set of Nats has minimum

Stream: new members

[Kent Van Vels]

I want to prove that a nonempty set of nats has a (unique) minimum.

Do I have to do a compactness/topological proof? Is there a better/easier way? I am planning on using this to show that infinite descent of nats is impossible so I would like to avoid using an infinite descent argument. Also I would like any recommendations for a better theorem name.

theorem min_exists_of_nonempty
(S: Set ℕ) : S.Nonempty → ∃ (n_min : S), (∀ (k:S), n_min ≤ k) := by
  intro h0
  sorry

I couldn't find the correct theorem in mathlib. Is there something similar there?

[Kent Van Vels]

This is what I did, after using the strong induction_on, I more or less followed my nose.

theorem min_exists_of_nonempty (S: Set ℕ) :
S.Nonempty → ∃ (n_min : ℕ), n_min ∈ S ∧ (∀ (k:ℕ), k ∈ S → n_min ≤ k) := by
  rintro ⟨x,h0⟩
  by_contra h1
  push_neg at h1
  induction' x using Nat.strong_induction_on with k hk
  rcases h1 k h0 with ⟨α,h2,h3⟩
  exact hk α h3 h2

[Daniel Weber]

You can use sInf for the infimum of the set, and then use docs#csInf_mem and docs#csInf_le'

[Kyle Miller]

theorem min_exists_of_nonempty (S : Set ℕ) (h : S.Nonempty) :
    ∃ (n_min : S), (∀ (k:S), n_min ≤ k) := by
  use! sInf S
  · exact Nat.sInf_mem h
  · simp only [Subtype.forall, Subtype.mk_le_mk]
    intro _ hs
    exact Nat.sInf_le hs

[Kyle Miller]

(That's meant to be pointers into the library)

[Kent Van Vels]

@Kyle Miller and @Daniel Weber, thank you both, I will look into this. I appreciate it.

[Kyle Miller]

docs#Nat.find is another more algorithmic way to express the infimum.

theorem min_exists_of_nonempty (S : Set ℕ) (h : S.Nonempty) :
    ∃ (n_min : S), (∀ (k:S), n_min ≤ k) := by
  classical
  use! Nat.find h
  · apply Nat.find_spec
  · simp only [Subtype.forall, Subtype.mk_le_mk]
    intro _ hs
    exact Nat.find_min' _ hs