Theorems · Theorem · general topology

Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt

∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
  IsCompact k → (∀ x ∈ k, ContinuousWithinAt f s x) → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

If a function is continuous within a set s at every point of a compact set k, then it is bounded on some open neighborhood of k in s.

Defined in

Mathlib.Topology.MetricSpace.Bounded

Cited by

2 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceTopologicalSpace