IsRetrocompact — Mathlib

English

If s and t are retrocompact, then their intersection s ∩ t is retrocompact.

Русский

Если s и t — ретро-компактные множества, то их пересечение s ∩ t тоже ретрокомпактно.

LaTeX

$$$\text{IsRetrocompact}(s) \land \text{IsRetrocompact}(t) \Rightarrow \text{IsRetrocompact}(s \cap t)$$$

Lean4

/-- A retrocompact set is a set whose intersection with every compact open is compact. -/
@[stacks 005A]
def IsRetrocompact (s : Set X) : Prop :=
  ∀ ⦃U⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)

Похожие утверждения