有空点赞我的视频哦:陶哲轩工作流之人工智能数学验证+定理发明工具LEAN4 [线性代数篇2前置知识]不同求和范围不同函数项结果相等的条件_哔哩哔哩_bilibili
-- 反向推理
refine' sum_bij _ _ _ _ _
-- {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β}
-- (i : ∀ a ∈ s, γ)
-- (hi : ∀ a ha, i a ha ∈ t)
-- (h : ∀ a ha, f a = g (i a ha))
-- (i_inj : ∀ a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-- (i_surj : ∀ b ∈ t, ∃ a ha, b = i a ha) :
-- ∏ x in s, f x = ∏ x in t, g x
-- 不一样的定义域s、t,不同的函数f、g,求和相同,需要什么条件呢。5个条件
-- 举例:
-- 假设我们有以下集合和映射:
-- 令 α = {1, 2, 3},即集合 {1, 2, 3}。 //s
-- 令 β = {a, b, c},即集合 {a, b, c}。 //
-- 令 γ = {x, y, z},即集合 {x, y, z}。 //t
-- 定义函数 f: α → β 和 g: γ → β 如下:
-- 对于 f,我们定义 f(1) = a,f(2) = b,f(3) = c。
-- 对于 g,我们定义 g(x) = a,g(y) = b,g(z) = c。
-- 接下来,定义函数 i: α → γ 如下:
-- i(1) = x
-- i(2) = y
-- i(3) = z
-- 现在,我们可以检查定理的条件是否满足:
-- 映射关系 (h): 对于所有 a 属于 {1, 2, 3},我们有 f a = g (i a)。
-- 这是满足的,例如,对于 a = 1,我们有 f(1) = a 和 g(i(1)) = g(x) = a。
-- i 是单射 (i_inj): 如果 i a₁ = i a₂,则 a₁ = a₂。
-- 这是满足的,因为 i 的定义是一对一的,不同的 a 映射到不同的 γ 中的元素。
-- i 是满射 (i_surj): 对于任意 b 属于 {x, y, z},存在 a 属于 {1, 2, 3},使得 b = i a。
-- 这也是满足的,因为 i 的定义覆盖了整个 γ。
-- 如果这些条件满足,我们可以应用定理,从而得出:
-- 即,
-- [
-- abc = abc文章来源:https://www.toymoban.com/news/detail-797290.html
-- ]文章来源地址https://www.toymoban.com/news/detail-797290.html
到了这里,关于陶哲轩工作流之人工智能数学验证+定理发明工具LEAN4 [线性代数篇2前置知识]不同求和范围不同函数项结果相等的条件的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!