comp_upperSemicontinuousOn — Mathlib

English

Let g be continuous, f be upper semicontinuous on s, and g monotone. Then g∘f is upper semicontinuous on s.

Русский

Пусть g непрерывна, f имеет верхнюю полупрерывность на s, и g монотонна. Тогда g∘f имеет верхнюю полупрерывность на s.

LaTeX

$$$hg : Continuous g,\\ hf : UpperSemicontinuousOn f s,\\ gmon : Monotone g\\Rightarrow\\; \\text{UpperSemicontinuousOn } (g \\circ f) s$$$

Lean4

theorem comp_upperSemicontinuousOn {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s)
    (gmon : Monotone g) : UpperSemicontinuousOn (g ∘ f) s := fun x hx =>
  hg.continuousAt.comp_upperSemicontinuousWithinAt (hf x hx) gmon

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