Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC