Theorems · Definition · general topology

Bornology.relativelyCompact

(X : Type u_1) → [inst : TopologicalSpace X] → [R0Space X] → Bornology X

In an R₀ space, relatively compact sets form a bornology. Its cobounded filter is Filter.coclosedCompact. See also Bornology.inCompact the bornology of sets contained in a compact set.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

3 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceR0Space