pi — Mathlib · SciLib

English

If for each i there is an equivalence e_i between Q_i and Q'_i, then there is a corresponding equivalence between pi Q and pi Q'.

Русский

Если для каждой i существует эквивалентность e_i между Q_i и Q'_i, тогда между pi Q и pi Q' существует эквивалентность.

LaTeX

$$$ (\\forall i, Q_i \\Equiv Q'_i) \\Rightarrow (\\pi Q) \\Equiv (\\pi Q'). $$$

Lean4

theorem pi [Fintype ι] {Q : ∀ i, QuadraticMap R (Mᵢ i) P} {Q' : ∀ i, QuadraticMap R (Nᵢ i) P}
    (e : ∀ i, (Q i).Equivalent (Q' i)) : (pi Q).Equivalent (pi Q') :=
  ⟨IsometryEquiv.pi fun i => Classical.choice (e i)⟩

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