continuous_sInf — Mathlib

English

If K is compact and f is continuous in the appropriate sense, then x ↦ sSup (f x '' K) is continuous.

Русский

Если K компактно и f непрерывна в нужном смысле, то x ↦ sSup(f x '' K) непрерывна.

LaTeX

$$$\\text{Continuous } x \\mapsto sSup(f(x) '' K)$$$

Lean4

theorem continuous_sInf {f : γ → β → α} {K : Set β} (hK : IsCompact K) (hf : Continuous ↿f) :
    Continuous fun x => sInf (f x '' K) :=
  IsCompact.continuous_sSup (α := αᵒᵈ) hK hf

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