isBounded_iff — Mathlib

English

In an R0 space, a set is bounded in the relatively compact bornology iff its closure is compact.

Русский

В R0-пространстве множество ограничено в борологии относительно компактного тогда и только тогда, когда его замыкание компактно.

LaTeX

$$$\\bigl( \\text{Bornology.IsBounded}_{relativelyCompact}(s) \\bigr) \\iff \\operatorname{IsCompact}(\\overline{s})$$$

Lean4

theorem isBounded_iff {s : Set X} : @Bornology.IsBounded _ (Bornology.relativelyCompact X) s ↔ IsCompact (closure s) :=
  compl_mem_coclosedCompact

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