ofIsCompl_add — Mathlib

English

Scaling the input maps by a scalar c scales the glued projection by c.

Русский

Умножение входа на скаляр c масштабирует слитое отображение на c.

LaTeX

$$$ofIsCompl\ h\ (c\cdot φ)\ (c\cdot ψ) = c\cdot (ofIsCompl\ h\ φ\ ψ).$$$

Lean4

@[simp]
theorem ofIsCompl_add (h : IsCompl p q) {φ₁ φ₂ : p →ₗ[R] F} {ψ₁ ψ₂ : q →ₗ[R] F} :
    ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂ :=
  ofIsCompl_eq _ (by simp) (by simp)

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