## Stream: Is there code for X?

### Topic: A strict_mono function from ℕ is determined by its image

#### Shing Tak Lam (Feb 27 2021 at 10:15):

import data.real.basic

lemma exists_of_range_eq_range {α : Type*} {f g : ℕ → α}
(hfg : set.range f = set.range g) (n : ℕ) :
∃ k, f n = g k :=
begin
have h₁ : f n ∈ set.range g,
{ simp [←hfg] },
rcases h₁ with ⟨t, ht⟩,
use t, rw ht
end

-- mainly looking for this one
lemma eq_of_strict_mono_of_range_eq {α : Type*} [linear_order α] {f g : ℕ → α} (hf : strict_mono f)
(hg : strict_mono g) (hfg : set.range f = set.range g) : f = g :=
begin
ext i,
apply nat.strong_induction_on i,
clear i,
intros i ih,
by_contra h,
cases ne.lt_or_lt h with h₁ h₁,
{ cases exists_of_range_eq_range hfg i with m hm,
have hmi : m < i,
{ rwa [hm, hg.lt_iff_lt] at h₁ },
specialize ih m hmi,
rwa [←hf.lt_iff_lt, hm, ih] at hmi,
exact lt_irrefl _ hmi },
{ cases exists_of_range_eq_range hfg.symm i with m hm,
have hmi : m < i,
{ rwa [hm, hf.lt_iff_lt] at h₁ },
specialize ih m hmi,
rwa [←hg.lt_iff_lt, hm, ih] at hmi,
exact lt_irrefl _ hmi }
end


I can't seem to find this in mathlib at the moment.

#### Heather Macbeth (Feb 27 2021 at 16:11):

Perhaps
https://leanprover-community.github.io/mathlib_docs/order/order_iso_nat.html
is useful. It contains related results. For example, your result is equivalent to the fact that the embedding constructed in docs#nat.order_embedding_of_set is unique.

#### Heather Macbeth (Feb 27 2021 at 16:22):

Another phrasing: there exists a unique strict-mono function (or, a unique order-iso) from ℕ to itself. It seems mathlib has these for fin:
docs#fin.strict_mono_unique
docs#fin.order_embedding_eq
but I don't see the result for ℕ.

Last updated: May 17 2021 at 16:26 UTC