人工智能数学验证工具LEAN4【入门介绍7】高级加法世界-如何进行分类讨论

视频链接:人工智能数学验证工具LEAN4【入门介绍7】高级加法世界-如何进行分类讨论_哔哩哔哩_bilibili

import Game.Levels.AdvAddition.L05add_right_eq_zero

World "AdvAddition"
Level 6
Title "add_left_eq_zero"

TheoremTab "+"

namespace MyNat

Introduction
"You can just mimic the previous proof to do this one -- or you can figure out a way
of using it.
"

/--  A proof that $a+b=0 \\implies b=0$. -/
TheoremDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "+"

/-- If $a+b=0$ then $b=0$. -/
Statement add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0 := by
  rw [add_comm]
  exact add_right_eq_zero b a

Conclusion "How about this for a proof:

```
rw [add_comm]
exact add_right_eq_zero b a
```

That's the end of Advanced Addition World! You'll need these theorems
for the next world, `≤` World. Click on \"Leave World\" to access it.
"

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/694357.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

[知识点]务必记住isBlank和isEnpty的区别!!!

身为一个伟大的程序员,我不允许你不懂isBlank和isEmpty的区别 正文 StrUtil.isBlank(message)和StrUtil.isEmpty(message)这两个方法都是用来检查一个字符串是否为空,但它们的行为是不同的: StrUtil.isEmpty(message):这个方法会检查字符串是…

数字化商品管理:革新鞋服零售模式,引领智能商业新时代

随着科技的快速发展,数字化浪潮席卷各行各业,鞋服零售企业亦不例外。在这个新时代,数字化商品管理不仅成为鞋服零售企业革新的关键,更是其引领智能商业浪潮的重要引擎。本文将围绕数字化商品管理如何深刻影响鞋服零售模式&#xf…

力扣 309. 买卖股票的最佳时机含冷冻期

题目来源:https://leetcode.cn/problems/best-time-to-buy-and-sell-stock-with-cooldown/description/ C题解:动态规划 状态1:表示持有股票。更新为之前持有股票(dp[i-1][0])或者不持有股票且不处于冷冻期后买入&…

Qt标准对话框设置

Qt标准对话框设置,设置字体、调色板、进度条等。 #include "mainwindow.h" #include "ui_mainwindow.h"MainWindow::MainWindow(QWidget *parent): QMainWindow(parent), ui(new Ui::MainWindow) {ui->setupUi(this); }MainWindow::~MainWi…

make_shared_for_overwrite

这个函数用来malloc数组,但不初始化。 不过这个仅限于内置类型。如果是用户写的,就会增加自动初始化(调用客户写的初始化)。

Java基于SSM的羽毛球馆管理系统,附源码

博主介绍:✌程序员徐师兄、7年大厂程序员经历。全网粉丝12w、csdn博客专家、掘金/华为云/阿里云/InfoQ等平台优质作者、专注于Java技术领域和毕业项目实战✌ 🍅文末获取源码联系🍅 👇🏻 精彩专栏推荐订阅👇…

[word] word带圈数字20以上 #笔记#笔记

word带圈数字20以上 办公中有时候需要用到带圈数字,超过20的数字就不能直接编辑了,那么20以上带圈数字要怎么输入呢?其实通过小技巧就能完成的,接下来就给大家介绍下呢,一起看看吧! 20以上带圈数字输入技巧…

Docker Compose 配置环境变量

在 Docker Compose 中, 可以通过 environment 字段来设置环境变量. 可以在 docker-compose.yml 文件中的服务定义中添加以下行来设置环境变量: services:myservice:environment:- "MY_VAR: myvalue"在这个例子中, myservice 服务的环境变量 MY_VAR 的值被设置为 myv…

Rust语言之异步写文件

文章目录 一、为什么用异步二、如何实现异步1.cargo.toml中引入Tokio2.代码实例 一、为什么用异步 将较与同步操作,异步操作则是非阻塞式的,当程序执行到异步操作时,它会立即返回并继续执行后续的代码,而不会等待该操作的完成。尤…

Java Swing游戏开发学习1

不使用游戏引擎,只使用Java SDK开发游戏的学习。 游戏原理 图片来自某大佬视频讲解 原理结合实际代码 public class GamePanel extends Jpanel implements Runnable {...run(){}// 详情看下图... }项目结构 运行效果 代码code 在我的下载里面可以找到&#xf…

devc++ 使用 winsock 实现 UDP 局域网 WIFI 广播

参考链接 使用UDP发送广播报_udp广播 inaddr_broadcast-CSDN博客 UDP接收端收不到广播的消息问题排查_unity upd广播连接不上是什么情况-CSDN博客 如何禁用自己电脑的虚拟网卡-百度经验 (baidu.com) 但是wifi 会屏蔽255.255.255.255 广播地址,所以 255.255.255.2…

USART(串口发送接受单字节)

一、硬件 差分信号不需要太大的压差。在相同的电磁干扰的环境下,因为是双扭线,两根线受干扰的程度是一样的,所以压差相对不变。提高抗干扰能力。485是双绞线传输取的是两线的压差。一般来说受干扰后同步变化,比如都升0.5V或都降5…

PROBIS铂思金融破产后续:ASIC牌照已注销

2024年1月31日,PROBIS铂思金融的澳大利亚ASIC牌照 (AFSL 338241) 被注销《差价合约经纪商PROBIS宣布破产,澳大利亚金融服务牌照遭暂停》,这也就意味着,PROBIS铂思金融目前已经没有任何金融牌照。 值得注意的是,时至今日…

k8s组件证书续期

K8S 各个组件需要与 api-server 进行通信,通信使用的证书都存放在 /etc/kubernetes/pki 路径下,由 kubeadm 生成的客户端证书在 1 年后到期,因此需要定时更新证书,否则证书到期会导致整个集群不可用。 证书过期后,执行kubectl命令会报如下错误: [root@k8s-master65 ~]#…

【Spring连载】使用Spring Data访问 MongoDB(四)----对象映射Object Mapping

【Spring连载】使用Spring Data访问 MongoDB(四)----对象映射Object Mapping 一、JSON Schema二、基于类型的转换器三、属性转换器四、非包装类型五、对象引用5.1 使用DBRefs 六、创建索引 一、JSON Schema 二、基于类型的转换器 三、属性转换器 四、…

Python实现线性逻辑回归和非线性逻辑回归

线性逻辑回归 # -*- coding: utf-8 -*- """ Created on 2024.2.20author: rubyw """import matplotlib.pyplot as plt import numpy as np from sklearn.metrics import classification_report from sklearn import preprocessing from sklearn…

【51单片机】利用【与或赋值法】优化【配置TMOD寄存器】

前言 大家好吖,欢迎来到 YY 滴单片机系列 ,热烈欢迎! 本章主要内容面向接触过单片机的老铁 本文是YY入门【【51单片机】从零开始手把手带你【查手册】配置定时器,并完成小项目(定时器&中断的应用&#xff0…

Spring整合Junit4

1、整合的好处 好处1&#xff1a;不需要自己创建IOC容器对象了好处2&#xff1a;任何需要的bean都可以在测试类中直接享受自动装配 2、操作 ①加入依赖 <dependency><groupId>junit</groupId><artifactId>junit</artifactId><version>4…

vmware升级处理vib包冲突的问题

一、问题截图 通过mgmt挂载iso: 通过vcenter升级的截图&#xff1a; 通过cli升级报错&#xff1a;二、解决办法 1、删除冲突的vib 2、重启后继续升级 三、解决步骤 1、查看那些vib冲突需要被清理 2、进行cli命令进行清理 esxcli software vib list | grep xxxx esxcli s…

hung task, soft lockup, hard lockup, workqueue stall

hung task&#xff0c;soft lockup&#xff0c;hard lockup&#xff0c;workqueue stall 是 linux 内核中的异常检测机制&#xff0c;这 4 个检测均是通过时间维度上的检测来判断异常。 在时间维度上的检测机制&#xff0c;有两个核心的点&#xff1a; &#xff08;1&#xff…