直播网站app下载,金华建设局政务网站,电子商务网站设计要求,网站必须做301重定向吗有空点赞我的视频哦#xff1a;陶哲轩工作流之人工智能数学验证定理发明工具LEAN4 [线性代数篇2前置知识]不同求和范围不同函数项结果相等的条件_哔哩哔哩_bilibili -- 反向推理
refine sum_bij _ _ _ _ _
-- {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β…有空点赞我的视频哦陶哲轩工作流之人工智能数学验证定理发明工具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) af(2) bf(3) c。
-- 对于 g我们定义 g(x) ag(y) bg(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
-- ]
