comp_upperSemicontinuous — Mathlib

English

If g is continuous, f is upper semicontinuous, and g is monotone, then the composition g∘f is upper semicontinuous.

Русский

Если g непрерывна, f имеет верхнюю полупрерывность, и g монотонна, тогда композиция g∘f обладает верхней полупрерывностью.

LaTeX

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

Lean4

theorem comp_upperSemicontinuous {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f)
    (gmon : Monotone g) : UpperSemicontinuous (g ∘ f) := fun x => hg.continuousAt.comp_upperSemicontinuousAt (hf x) gmon

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