pi — Mathlib · SciLib

English

If for every index i, the components x i and y i commute, then the pi-valued x and y commute.

Русский

Если для каждого i компонентам x_i и y_i удовлетворяется коммутативность, то x и y в Pi-компонентах commute.

LaTeX

$$$\forall i, \mathrm{Commute}(x_i, y_i) \Rightarrow \mathrm{Commute}(x, y)$$$

Lean4

@[to_additive]
theorem pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y :=
  SemiconjBy.pi h

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