IsComplete.isClosed

theorem IsComplete.isClosed : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α] {s : Set α}, IsComplete s → IsClosed s

This theorem states that in a separated space (also known as a T0 space), a complete set is always closed. Here, a set is complete if for any Cauchy filter on the set, there exists a limit in the set. In this context, a set is closed if its complement is open. A space is separated, or T0, if for any two distinct points, there exists a neighborhood that contains one but not the other.

More concisely: In a separated (T0) space, every complete set is closed.