exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn

English

If a function is continuous at every point of a compact set k, there exists an open set t with k ⊆ t such that f''t is bounded.

Русский

Если функция непрерывна в каждой точке компактного множества k, существует открытое множество t с k ⊆ t, такое что образ f''t ограничен.

LaTeX

$$$\\\\forall {k s}\\\\IsCompact k \\\\Rightarrow (\\\\forall x \\in k, ContinuousAt f x) \\\\Rightarrow \\\\exists t, k \\subseteq t \\land IsOpen t \\land IsBounded(f''t).$$$

Lean4

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

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