Theorems · Theorem · operator theory

isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image

∀ {M₁ : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [T2Space M₂] (f : M₁ → M₂),
  IsCompactOperator f ↔ ∃ V ∈ nhds 0, IsCompact (closure (f '' V))

Defined in

Mathlib.Analysis.Normed.Operator.Compact.Basic

Cited by

2 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommMonoidTopologicalSpaceT2Space