add — Mathlib

English

If f and g are compact operators and the ambient space allows, then f − g is compact.

Русский

Если f и g компактны и множество условий позволяют, то f − g компактно.

LaTeX

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

Lean4

theorem add [ContinuousAdd M₂] {f g : M₁ → M₂} (hf : IsCompactOperator f) (hg : IsCompactOperator g) :
    IsCompactOperator (f + g) :=
  let ⟨A, hA, hAf⟩ := hf
  let ⟨B, hB, hBg⟩ := hg
  ⟨A + B, hA.add hB, mem_of_superset (inter_mem hAf hBg) fun _ ⟨hxA, hxB⟩ => Set.add_mem_add hxA hxB⟩

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