English
A subset s of a topological space is quasi-separated if the intersection of any pair of open compact subsets of s is compact.
Русский
Подмножество s в топологическом пространстве называется квазисьергированным, если пересечение любых двух открытых компактных подмножеств s остается компактным.
LaTeX
$$$\mathrm{IsQuasiSeparated}(s) \;\equiv\; \forall U,V\; (U\subseteq s)\;\text{IsOpen}(U)\to\text{IsCompact}(U)\ ,\ (V\subseteq s)\;\text{IsOpen}(V)\to\text{IsCompact}(V)\Rightarrow \text{IsCompact}(U\cap V).$$$
Lean4
/-- A subset `s` of a topological space is quasi-separated if the intersections of any pairs of
compact open subsets of `s` are still compact.
Note that this is equivalent to `s` being a `QuasiSeparatedSpace` only when `s` is open. -/
def IsQuasiSeparated (s : Set α) : Prop :=
∀ U V : Set α, U ⊆ s → IsOpen U → IsCompact U → V ⊆ s → IsOpen V → IsCompact V → IsCompact (U ∩ V)
