English
If 0 < c < 1/2, then cantorFunction(c) is injective on binary sequences f,g : N → Bool; i.e., cantorFunction(c) f = cantorFunction(c) g implies f = g.
Русский
Если 0 < c < 1/2, то CantorFunction(c) инъективна на пространстве бинарных последовательностей f,g : N → {0,1}. То есть равенство CantorFunction(c) f = CantorFunction(c) g влечет равенство f = g.
LaTeX
$$$0 < c < \frac{1}{2} \Rightarrow \forall f,g : \mathbb{N} \to \{0,1\}, \ CantorFunction(c)\,f = CantorFunction(c)\,g \Rightarrow f = g$$$
Lean4
/-- `cantorFunction c` is injective if `0 < c < 1/2`. -/
theorem cantorFunction_injective (h1 : 0 < c) (h2 : c < 1 / 2) : Function.Injective (cantorFunction c) :=
by
intro f g hfg
classical
contrapose hfg with h
have : ∃ n, f n ≠ g n := Function.ne_iff.mp h
let n := Nat.find this
have hn : ∀ k : ℕ, k < n → f k = g k := by
intro k hk
apply of_not_not
exact Nat.find_min this hk
cases fn : f n
· apply _root_.ne_of_lt
refine increasing_cantorFunction h1 h2 hn fn ?_
apply Bool.eq_true_of_not_eq_false
rw [← fn]
apply Ne.symm
exact Nat.find_spec this
· apply _root_.ne_of_gt
refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn
apply Bool.eq_false_of_not_eq_true
rw [← fn]
apply Ne.symm
exact Nat.find_spec this
