We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 34a182f commit 167aaa4Copy full SHA for 167aaa4
Mathlib/Topology/Instances/Matrix.lean
@@ -69,7 +69,6 @@ theorem IsCompact.matrix [TopologicalSpace R] {S : Set R} (hS : IsCompact S) :
69
IsCompact (S.matrix : Set (Matrix m n R)) :=
70
isCompact_pi_infinite fun _ => isCompact_pi_infinite fun _ => hS
71
72
-
73
end Set
74
75
/-! ### Lemmas about continuity of operations -/
0 commit comments