## Stream: new members

### Topic: Find min of a set of natural numbers

#### Ryan Lahfa (Apr 04 2020 at 21:50):

I'm trying to understand the nat.find_xxx API and as far as I understand it, it looks like rather some helpers which prove the induction over natural numbers.

I have some set of natural numbers which is infinite, nonempty and I'd like to take the smallest element, I could reuse the Inf/is_least machinery but I think there must be more elementary things to do?

Namely, I'm interested in this (mis-formulated?) lemma:

import data.set

lemma smallest_element (S: set ℕ): S.nonempty → ∃ n : ℕ, ∀ m < n, m \notin S := sorry


#### Ryan Lahfa (Apr 04 2020 at 21:50):

(I cannot use finset.min because of the infinite condition.)

#### Ryan Lahfa (Apr 04 2020 at 21:53):

lemma smallest_element (S: set ℕ): S.nonempty → ∃ n : ℕ, ∀ m < n, m ∉ S := begin
intro H,
use (nat.find H),
intro m,
apply nat.find_min H,
end


seems to work just fine.

But I wonder if there is a more canonical way.

#### Daniel Keys (Apr 04 2020 at 23:00):

Well-ordered principle: every non-empty subset of the natural numbers has a least element.

#### Daniel Keys (Apr 04 2020 at 23:02):

Mathematical induction is true if and only if ℕ is well-ordered.

#### Ryan Lahfa (Apr 04 2020 at 23:12):

Daniel Keys said:

Well-ordered principle: every non-empty subset of the natural numbers has a least element.

Is there a direct theorem using is_least?

#### Daniel Keys (Apr 04 2020 at 23:42):

Not sure what you mean here, but it seems to me that your smallest_element lemma restates an axiom:

axiom well_ordered (S : set ℕ) : S.nonempty → ∃ m ∈ S, ∀ n ∈ S, m ≤ n


#### Kevin Buzzard (Apr 04 2020 at 23:43):

That's not an axiom in Lean

that's a theorem

#### Daniel Keys (Apr 04 2020 at 23:44):

Good point. I didn't mean it was in Lean.

#### Kevin Buzzard (Apr 04 2020 at 23:45):

The question is how to do all of this stuff in Lean.

#### Daniel Keys (Apr 04 2020 at 23:46):

Isn't this hidden somewhere in Lean - i.e. by the definition of the naturals as an inductive type?

Sure

#### Kevin Buzzard (Apr 04 2020 at 23:46):

The question is where is it hidden and what is the canonical way to get it out.

#### Kevin Buzzard (Apr 04 2020 at 23:47):

< is not some predicate which is canonically associated to nat; < has a definition which probably uses +

(deleted)

#### Logan Murphy (Nov 26 2020 at 15:26):

I hope it's okay to revive an old thread, but I wanted to write a proof of the well-ordering principle for positive naturals and so was searching through old Zulip threads mentioning WOP, of which there are a few. I ended up figuring out this (not particularly graceful) tactic proof, so I thought I'd stick it here in case anyone else tries looking up "well-ordering principle" and finds it useful.

import tactic
open classical

local attribute [instance] prop_decidable

lemma pnat_wf : well_founded (preorder.to_has_lt ℕ+).1 :=
measure_wf coe

lemma well_ordering_principle (A : set pnat) : A.nonempty →
∃ m ∈ A, (∀ x ∈ A, m ≤ x) :=
begin
intro H,
have := well_founded.has_min pnat_wf A H,
rcases this with ⟨m, H1,H2⟩,
use m, split,{exact H1},
intros x H3, replace H2 := H2 x H3,
exact not_lt.mp H2,
end


#### Mario Carneiro (Nov 26 2020 at 15:31):

FYI, "well ordering principle" is another way to spell "induction"

Last updated: May 16 2021 at 21:11 UTC