mathlib

a80e1d71 - chore(topology/metric_space): split `iff` into 2 lemmas (#9238)

chore(topology/metric_space): split `iff` into 2 lemmas (#9238) One of the implications of `compact_iff_closed_bounded` doesn't need `t2_space`. Also add `compact_space_iff_bounded_univ`.