WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Closed graph theorem (functional analysis)

Revision #1084 → #2223 · back to history

modifiedPseudometrizable metrizable iff Hausdorff7837043b7fc1
FieldFrom #1084To #2223
mathlib.declPseudoMetrizableSpace.toMetrizableSpaceTopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace
noteBoth implications exist as instances (T0/Hausdorff pseudometrizable → metrizable, and metrizable → T2), but not packaged as a single biconditional.The T0/Hausdorff pseudometrizable → metrizable direction exists as an instance, and metrizable → T2 holds, but the biconditional is not packaged as one statement.
addedClosed linear operatord4806e8e6a88