comp_lowerSemicontinuous — Mathlib

English

If g is antitone and continuous at f(x), then g∘f is upper semicontinuous at x given lower semicontinuity of f.

Русский

Если g антимонотонна и непрерывна в f(x), тогда g∘f является верхней полупрерывностью в x при наличии нижней полупрерывности f.

LaTeX

$$$\\text{ContinuousAt } g (f x) \\land \\text{LowerSemicontinuousAt } f x \\Rightarrow \\text{UpperSemicontinuousAt } (g∘f) x$$$

Lean4

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

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