isCompact — Mathlib

English

If A is compact and B is exposed with respect to A (under suitable topological hypotheses), then B is compact.

Русский

Если A компактно, и B экспонировано относительно A (при соблюдении соответствующих условий), то B компактно.

LaTeX

$$$$ IsExposed\ 𝕜\ A\ B \to IsCompact\ A \to IsCompact\ B. $$$$

Lean4

protected theorem isCompact [OrderClosedTopology 𝕜] [T2Space E] {A B : Set E} (hAB : IsExposed 𝕜 A B)
    (hA : IsCompact A) : IsCompact B :=
  hA.of_isClosed_subset (hAB.isClosed hA.isClosed) hAB.subset

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