comp_lowerSemicontinuousOn — Mathlib

English

If g is continuous at x and f is lower semicontinuous at g(x), then g∘f is lower semicontinuous at x.

Русский

Если g непрерывна в x и f — нижне полупрерывна в g(x), то g∘f — нижне полупрерывна в x.

LaTeX

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

Lean4

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

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