inner_single_left — Mathlib

English

Analogously, ⟪f, lp.single 2 i a⟫ = ⟪f(i), a⟫ for f in lp G 2.

Русский

Аналогично, ⟪f, lp.single 2 i a⟫ = ⟪f(i), a⟫ для f в lp G 2.

LaTeX

$$$ \\langle f, \\; lp.single 2 i a \\rangle = \\langle f(i), a \\rangle $$$

Lean4

theorem inner_single_left [DecidableEq ι] (i : ι) (a : G i) (f : lp G 2) : ⟪lp.single 2 i a, f⟫ = ⟪a, f i⟫ :=
  by
  refine (hasSum_inner (lp.single 2 i a) f).unique ?_
  simp_rw [lp.coeFn_single]
  convert hasSum_ite_eq i ⟪a, f i⟫ using 1
  ext j
  split_ifs with h
  · subst h; rw [Pi.single_eq_same]
  · simp [Pi.single_eq_of_ne h]

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