exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt

English

If a function is continuous on s at every point of a compact set k, then there exists an open neighborhood t of k in s such that f''(t ∩ s) is bounded.

Русский

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

LaTeX

$$$\\exists t\\, (k \\subseteq t) \\land IsOpen t \\land IsBounded(f''(t \\cap s)).$$$

Lean4

/-- If a function is continuous at every point of a compact set `k`, then it is bounded on
some open neighborhood of `k`. -/
theorem exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt [TopologicalSpace β] {k : Set β} {f : β → α}
    (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousAt f x) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t) :=
  by
  simp_rw [← continuousWithinAt_univ] at hf
  simpa only [inter_univ] using exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf

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