pi_midpoint_apply — Mathlib

English

For a family of points f,g in a product space, the component i of their midpoint agrees with the midpoint of the i-th components.

Русский

Для семейства точек f,g в произведении компонент i середины равен середине компонентов i-й координаты.

LaTeX

$$$ \forall i,\ \operatorname{midpoint} k f g i = \operatorname{midpoint} k (f i) (g i) $$$

Lean4

@[simp]
theorem pi_midpoint_apply {k ι : Type*} {V : ι → Type*} {P : ι → Type*} [Ring k] [Invertible (2 : k)]
    [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)] [∀ i, AddTorsor (V i) (P i)] (f g : ∀ i, P i) (i : ι) :
    midpoint k f g i = midpoint k (f i) (g i) :=
  rfl

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