comp_upperSemicontinuous_antitone

English

If hg is continuous, hf is upper semicontinuous on s at x, and gmon is Monotone, then the composition g∘f is upper semicontinuous on s at x.

Русский

Если hg непрерывна, hf верхняя полупрерывность на s в x и g монотонна, тогда g∘f верхняя полупрерывность на s в x.

LaTeX

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

Lean4

theorem comp_upperSemicontinuous_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuous f)
    (gmon : Antitone g) : LowerSemicontinuous (g ∘ f) := fun x =>
  hg.continuousAt.comp_upperSemicontinuousAt_antitone (hf x) gmon

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