comp_lowerSemicontinuousAt — Mathlib

English

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

Русский

Если g непрерывно в точке f(x) и f – нижне полупрерывна в x, и g монотонна, то g∘f остается нижне полупрерывной в x.

LaTeX

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

Lean4

theorem comp_lowerSemicontinuousAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousAt f x)
    (gmon : Monotone g) : LowerSemicontinuousAt (g ∘ f) x :=
  by
  simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
  exact hg.comp_lowerSemicontinuousWithinAt hf gmon

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