contLinear_map_vsub — Mathlib

English

Continuity of the linear part respects addition and scalar multiplication.

Русский

Линейная часть сохраняет сложение и умножение на скаляры при непрерывности.

LaTeX

$$$f.contLinear$ preserves linear structure and continuity$$

Lean4

@[simp]
theorem contLinear_map_vsub (f : P →ᴬ[R] Q) (p₁ p₂ : P) : f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂ :=
  f.toAffineMap.linearMap_vsub p₁ p₂

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