Commit 2025-07-26 23:35 ce6e378d

View on Github →

feat(Topology/Instances/Matrix): topology of Set.matrix (#27496) Prove topological results (IsOpen, IsCompact) about Set.matrix.

Estimated changes

added theorem Set.matrix_eq_pi
added theorem IsCompact.matrix
added theorem IsOpen.matrix