Theorems · Definition · operator theory

IsCompactOperator

{M₁ : Type u_1} → {M₂ : Type u_2} → [Zero M₁] → [TopologicalSpace M₁] → [TopologicalSpace M₂] → (M₁ → M₂) → Prop

A compact operator between two topological vector spaces. This definition is usually given as "there exists a neighborhood of zero whose image is contained in a compact set", but we choose a definition which involves fewer existential quantifiers and replaces images with preimages. We prove the equivalence in isCompactOperator_iff_exists_mem_nhds_image_subset_compact.

Defined in

Mathlib.Analysis.Normed.Operator.Compact.Basic

Cited by

51 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

ZeroTopologicalSpaceTopologicalSpace