relativelyCompact_eq_inCompact — Mathlib

English

In an R1 space, the relatively compact bornology coincides with the inCompact bornology.

Русский

В R1-пространстве относительно компактная борология совпадает с борологией inCompact.

LaTeX

$$Bornology.relativelyCompact X = Bornology.inCompact X$$

Lean4

/-- In an R₁ space, the bornologies `relativelyCompact` and `inCompact` are equal. -/
@[simp]
theorem relativelyCompact_eq_inCompact : Bornology.relativelyCompact X = Bornology.inCompact X :=
  Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact

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