English
If f is StrictMono and h is a well-founded LT, then the range of f is injective on the domain; i.e., f is determined by its range on that set.
Русский
Пусть f строго монотонна; тогда ее область значений инъективна относительно диапазона; то есть если два аргумента дают одинаковый диапазон, то функции равны.
LaTeX
$$$\\text{Set.InjOn }\\text{Set.range }\\{f:\\beta\\to\\gamma \\mid \\text{StrictMono } f\\}$$$
Lean4
theorem range_injOn_strictMono [WellFoundedLT β] : Set.InjOn Set.range {f : β → γ | StrictMono f} :=
by
intro f hf g hg hfg
ext a
apply WellFoundedLT.induction a
intro a IH
obtain ⟨b, hb⟩ := hfg ▸ mem_range_self a
obtain h | rfl | h := lt_trichotomy b a
· rw [← IH b h] at hb
cases (hf.injective hb).not_lt h
· rw [hb]
· obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a
have := hg h
rw [hb, ← hc, hf.lt_iff_lt] at this
rw [IH c this] at hc
cases (hg.injective hc).not_lt this
