isCompactOperator_zero — Mathlib

English

Let M1 and M2 be topological spaces with a distinguished zero map. The zero linear map 0: M1 → M2 is a compact operator because its image is the singleton {0}, which is compact.

Русский

Пусть M1 и M2 — топологические пространства. Нулевое линейное отображение 0: M1 → M2 является компактным оператором, так как образом является единичный множество {0}, компактное.

LaTeX

$$$IsCompactOperator(0 : M_1 \to M_2)$$$

Lean4

theorem isCompactOperator_zero {M₁ M₂ : Type*} [Zero M₁] [TopologicalSpace M₁] [TopologicalSpace M₂] [Zero M₂] :
    IsCompactOperator (0 : M₁ → M₂) :=
  ⟨{0}, isCompact_singleton, mem_of_superset univ_mem fun _ _ => rfl⟩

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