greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update README.md

Browse Source
This commit is contained in:
Jon Eugster
2024-03-21 14:43:03 +01:00
committed by Hydrogenbear
parent a21ba830f5
commit 1c993b95ef
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.i18n/zh/Game.po
View File

@@ -2513,7 +2513,7 @@ msgstr ""
"\n" "\n"
"你可以把 `succ_inj` 本身看作是一个证明；它是 `succ` 是一个单射函数的证明。换句话说，\n" "你可以把 `succ_inj` 本身看作是一个证明；它是 `succ` 是一个单射函数的证明。换句话说，\n"
"`succ_inj` 是\n" "`succ_inj` 是\n"
"$ \forall a, b \\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b $ 的证明。\n" "$ \\forall a, b \\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b $ 的证明。\n"
"\n" "\n"
"`succ_inj` 被皮亚诺假设为一个公理，但在 Lean 中可以使用 `pred` 来证明，这是一个在数学上有病态的函数。" "`succ_inj` 被皮亚诺假设为一个公理，但在 Lean 中可以使用 `pred` 来证明，这是一个在数学上有病态的函数。"