We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b7d0d23 commit c3d8502Copy full SHA for c3d8502
1 file changed
Mathlib/Analysis/Normed/Operator/Compact.lean
@@ -69,7 +69,8 @@ theorem isCompactOperator_zero {M₁ M₂ : Type*} [Zero M₁] [TopologicalSpace
69
⟨{0}, isCompact_singleton, mem_of_superset univ_mem fun _ _ => rfl⟩
70
71
/--
72
-The identity of a topological additive group is a compact operator implies it is weakly locally compact.
+The identity of a topological additive group is a compact operator implies it is weakly
73
+locally compact.
74
-/
75
lemma WeaklyLocallyCompactSpace.of_isCompactOperator_id
76
{M₁ : Type*} [TopologicalSpace M₁] [AddCommGroup M₁] [ContinuousAdd M₁]
0 commit comments