brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2024-09-19 06:05:14 -04:00
Code Issues Projects Releases Packages Wiki Activity

Small proof change

Browse source
This commit is contained in:
Brandon Rozek 2024-04-16 22:02:34 -04:00
parent da6c10ed82
commit 597fab929b
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
content/blog/functions-inductive-propositions-lean4.md
View file

@ -152,7 +152,7 @@ Since we don't know how to show whether collatz terminates, we can't at this tim
```lean ```lean
theorem collatz_sound (n r : Nat) : (∃ t, collatz_fun n t = some r) → collatz n r := by theorem collatz_sound (n r : Nat) : (∃ t, collatz_fun n t = some r) → collatz n r := by
intro (H: ∃ t, collatz_fun n t = some r) intro (H: ∃ t, collatz_fun n t = some r)
cases' H with t H obtain ⟨t, H⟩ := H
revert H n r revert H n r
show ∀ (n r : Nat), collatz_fun n t = some r → collatz n r show ∀ (n r : Nat), collatz_fun n t = some r → collatz n r