inner_eq_inner — Mathlib

English

If x1 is inseparable from x2 and y1 from y2, then the inner product respects inseparability: ⟪x1,y1⟫ = ⟪x2,y2⟫.

Русский

Если x1 inseparable от x2 и y1 inseparable от y2, то скалярное произведение сохраняет равенство: ⟪x1,y1⟫ = ⟪x2,y2⟫.

LaTeX

$$$\langle x_1,y_1\rangle = \langle x_2,y_2\rangle.$$$

Lean4

theorem inner_eq_inner {x₁ x₂ y₁ y₂ : E} (hx : Inseparable x₁ x₂) (hy : Inseparable y₁ y₂) : ⟪x₁, y₁⟫ = ⟪x₂, y₂⟫ :=
  ((hx.prod hy).map continuous_inner).eq

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