`BookProof.ChapterSeparableSpectrum.metrizableSpace_of_separable_continuousMap` [SeparableSpace C(Y, ℂ)] : MetrizableSpace Y

Initializing...

`BookProof.ChapterSeparableSpectrum.metrizableSpace_of_separable_continuousMap` [SeparableSpace C(Y, ℂ)] : MetrizableSpace Y · Prove2Me