Theorems · Definition · general topology

IsCompact

{X : Type u_1} → [TopologicalSpace X] → Set X → Prop

A set s is compact if for every nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

1,282 results in Mathlib

Foundations

Depth 49 from the axioms, rests on 540 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace