prod_single_index — Mathlib

English

Let a ∈ α, b ∈ M, and h: α → M → N with h(a,0) = 1. Then (single a b).prod h = h a b.

Русский

Пусть a ∈ α, b ∈ M, и h: α → M → N с h(a,0) = 1. Тогда (single a b).prod h = h a b.

LaTeX

$$$ h_{zero} : h a 0 = 1 \\\\Rightarrow (single a b).prod h = h a b $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_single_index {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) : (single a b).prod h = h a b :=
  calc
    (single a b).prod h = ∏ x ∈ { a }, h x (single a b x) :=
      prod_of_support_subset _ support_single_subset h fun _ hx => (mem_singleton.1 hx).symm ▸ h_zero
    _ = h a b := by simp

Похожие утверждения