relativelyCompact — Mathlib

English

The Pi-space of a family of R0 spaces is R0.

Русский

Произведение по индексному множеству из пространств R0 образует R0-пространство.

LaTeX

$$$R0Space(\\forall i, X_i)$$$

Lean4

/-- 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. -/
def relativelyCompact : Bornology X where
  cobounded := Filter.coclosedCompact X
  le_cofinite := Filter.coclosedCompact_le_cofinite

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