pi — Mathlib · SciLib

English

The componentwise semiconjugacy lifts to the pi-type: if for every i, SemiconjBy (x i) (y i) (z i), then SemiconjBy x y z.

Русский

Пусть для каждого i выполняется полу-сопряжённость: SemiconjBy (x i) (y i) (z i); тогда она выполняется и для функций x, y, z, то есть SemiconjBy x y z.

LaTeX

$$$\big(\forall i, \mathrm{SemiconjBy}(x_i, y_i, z_i)\big) \Rightarrow \mathrm{SemiconjBy}(x, y, z)$$$

Lean4

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

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