Theorem isCompactOperator_id_iff_locallyCompactSpace

Modification history

2026-02-18 19:37
Mathlib/Analysis/Normed/Operator/Compact.lean
feat(Analysis/Normed/Operator/Compact): criteria for compactness of the identity operator (#35196) …
Added isCompactOperator_id_iff_locallyCompactSpaceView on Github →