English
If f is a continuous function of two variables on a compact set K, then the function x ↦ sSup (f(x)''K) is continuous.
Русский
Если функция f непрерывна по двум переменным на компактном множестве K, то функция x ↦ sSup(f(x)''K) непрерывна.
LaTeX
$$Continuous (x \\mapsto sSup (f(x) '' K))$$
Lean4
/-- If `f : γ → β → α` is a function that is continuous as a function on `γ × β`, `α` is a
conditionally complete linear order, and `K : Set β` is a compact set, then
`fun x ↦ sSup (f x '' K)` is a continuous function. -/
/- TODO: generalize. The following version seems to be true:
```
theorem IsCompact.tendsto_sSup {f : γ → β → α} {g : β → α} {K : Set β} {l : Filter γ}
(hK : IsCompact K) (hf : ∀ y ∈ K, Tendsto ↿f (l ×ˢ 𝓝[K] y) (𝓝 (g y)))
(hgc : ContinuousOn g K) :
Tendsto (fun x => sSup (f x '' K)) l (𝓝 (sSup (g '' K))) := _
```
Moreover, it seems that `hgc` follows from `hf` (Yury Kudryashov). -/
theorem continuous_sSup {f : γ → β → α} {K : Set β} (hK : IsCompact K) (hf : Continuous ↿f) :
Continuous fun x => sSup (f x '' K) :=
by
rcases eq_empty_or_nonempty K with (rfl | h0K)
· simp_rw [image_empty]
exact continuous_const
rw [continuous_iff_continuousAt]
intro x
obtain ⟨y, hyK, h2y, hy⟩ :=
hK.exists_sSup_image_eq_and_ge h0K (show Continuous (f x) from hf.comp <| .prodMk_right x).continuousOn
rw [ContinuousAt, h2y, tendsto_order]
have := tendsto_order.mp ((show Continuous fun x => f x y from hf.comp <| .prodMk_left _).tendsto x)
refine ⟨fun z hz => ?_, fun z hz => ?_⟩
· refine (this.1 z hz).mono fun x' hx' => hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn
· have h : ({ x } : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z :=
by
rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
exact (hy y' hy').trans_lt hz
obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ := generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h
refine eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_
rw [hK.sSup_lt_iff_of_continuous h0K (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]
exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))
