smul — Mathlib

English

If f and g are compact operators, then their sum f + g is compact.

Русский

Если f и g — компактные операторы, то их сумма f + g компактна.

LaTeX

$$$IsCompactOperator(f) \land IsCompactOperator(g) \Rightarrow IsCompactOperator(f + g)$$$

Lean4

theorem smul {S : Type*} [Monoid S] [DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂}
    (hf : IsCompactOperator f) (c : S) : IsCompactOperator (c • f) :=
  let ⟨K, hK, hKf⟩ := hf
  ⟨c • K, hK.image <| continuous_id.const_smul c, mem_of_superset hKf fun _ hx => smul_mem_smul_set hx⟩

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