Theorem isOpen_setOf_nat_le_rank

Modification history

2023-05-20 01:06

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

feat: port Analysis.NormedSpace.FiniteDimension (#4123)

Added isOpen_setOf_nat_le_rank View on Github →