exists_isOpen_isBounded_image_of_isCompact_of_continuousOn

English

In a proper Hausdorff space, a set is compact if and only if it is closed and bounded.

Русский

В корректном (правдоподобном) гомотетическом пространстве Хаусдорфа множество компактно тогда и только тогда, когда оно замкнуто и ограничено.

LaTeX

$$$IsCompact(s) \\iff (IsClosed(s) \\land IsBounded(s)).$$$

Lean4

/-- If a function is continuous on a neighborhood of a compact set `k`, then it is bounded on
some open neighborhood of `k`. -/
theorem exists_isOpen_isBounded_image_of_isCompact_of_continuousOn [TopologicalSpace β] {k s : Set β} {f : β → α}
    (hk : IsCompact k) (hs : IsOpen s) (hks : k ⊆ s) (hf : ContinuousOn f s) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t) :=
  exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt hk fun _x hx =>
    hf.continuousAt (hs.mem_nhds (hks hx))

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