English
If g is continuous at f(x), f is upper semicontinuous within a set s at x, and g is monotone, then the composition g∘f is upper semicontinuous within s at x.
Русский
Если g непрерывна в точке f(x), f имеет верхнюю полупрерывность внутри множества s в точке x, и g монотонна, то композиция g∘f имеет верхнюю полупрерывность внутри s в x.
LaTeX
$$$hg : \\text{ContinuousAt } g (f x),\\ hf : \\text{UpperSemicontinuousWithinAt } f\ts x,\n\\ gmon : \\text{Monotone } g \\;\\Rightarrow\\; \\text{UpperSemicontinuousWithinAt } (g \\circ f) s x$$$
Lean4
theorem comp_upperSemicontinuousWithinAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
(hf : UpperSemicontinuousWithinAt f s x) (gmon : Monotone g) : UpperSemicontinuousWithinAt (g ∘ f) s x :=
@ContinuousAt.comp_lowerSemicontinuousWithinAt α _ x s γᵒᵈ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon.dual
