Mathlib v3 is deprecated. Go to Mathlib v4

Theorem minimal_nonempty_closed_eq_singleton

Modification history

2022-05-23 01:49
src/topology/separation.lean
chore(topology/separation): golf some proofs (#14279) …
Added minimal_nonempty_closed_eq_singletonView on Github →