Latest video is up!
This time we look at proving a (simple!) theorem that has an inequality in its hypotheses ..
... that requires us to learn about a new tactic "rel" to reason about inequalities.
youtube:
https://www.youtube.com/watch?v=lcjF1DerqQ4
blog: https://leanfirststeps.blogspot.com/2024/07/05-inequalities.html
#maths #lean #lean4
Tariq /
npub1xs…ctf6m
2024-07-08 22:58:50
Author Public Key
npub1xsrfffw8z907pyv0ulkfqwrcvkfw8qz0rg8y2l37p8gran76m34s2ctf6mPublished at
2024-07-08 22:58:50Event JSON
{
"id": "09a63279de9e722d2496a658a36d7c8a2561c263dfff10ac286ac4c26994743a",
"pubkey": "340694a5c7115fe0918fe7ec9038786592e3804f1a0e457e3e09d03ecfdadc6b",
"created_at": 1720479530,
"kind": 1,
"tags": [
[
"t",
"maths"
],
[
"t",
"lean"
],
[
"t",
"lean4"
],
[
"proxy",
"https://mastodon.social/users/rzeta0/statuses/112753346497470660",
"activitypub"
]
],
"content": "Latest video is up!\n\nThis time we look at proving a (simple!) theorem that has an inequality in its hypotheses .. \n\n... that requires us to learn about a new tactic \"rel\" to reason about inequalities.\n\nyoutube: \nhttps://www.youtube.com/watch?v=lcjF1DerqQ4\n\nblog: https://leanfirststeps.blogspot.com/2024/07/05-inequalities.html\n\n#maths #lean #lean4",
"sig": "30fa6be6f6f16e5ae513be944cfb5a7395d1e607142604d9ff0f80d9ffd6dcced543836bec78cb7e7500a6f1730bbf73cdcf458077618e82f5a3abf6930faa67"
}