comp_continuous — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_continuous {f : α → β} {g : ι → α} (hf : LowerSemicontinuous f) (hg : Continuous g) :
    LowerSemicontinuous fun x ↦ f (g x) := fun x ↦ (hf (g x)).comp_continuousAt hg.continuousAt

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