exists_bound_of_continuousOn' — Mathlib

English

If IsCompact s and f is continuous on s, then there exists C with ∥f(x)∥ ≤ C for all x in s.

Русский

Если s компактно, а f непрерывна на s, то найдется C, такой что ∥f(x)∥ ≤ C для всех x в s.

LaTeX

$$∃ C, ∀ x ∈ s, ∥f(x)∥ ≤ C$$

Lean4

@[to_additive IsCompact.exists_bound_of_continuousOn]
theorem exists_bound_of_continuousOn' [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E}
    (hf : ContinuousOn f s) : ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C :=
  (isBounded_iff_forall_norm_le'.1 (hs.image_of_continuousOn hf).isBounded).imp fun _C hC _x hx =>
    hC _ <| Set.mem_image_of_mem _ hx

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