Theorem isCompact_iff_ultrafilter_le_nhds'

Modification history

2023-10-29 04:04
Mathlib/Topology/Compactness/Compact.lean
feat: a unique cluster pt of a filter is its limit (#7944) …
Added isCompact_iff_ultrafilter_le_nhds'View on Github →