comp_continuousAt_of_eq — Mathlib

English

If f is lower semicontinuous and g is continuous, then g∘f is lower semicontinuous.

Русский

Если f — нижняя полупрерывная, а g — непрерывна, тогда g∘f — нижняя полупрерывная.

LaTeX

$$$\\text{LowerSemicontinuous } f \\Rightarrow \\text{Continuous } g \\Rightarrow \\text{LowerSemicontinuous } (g∘f)$$$

Lean4

theorem comp_continuousAt_of_eq {f : α → β} {g : ι → α} {y : α} {x : ι} (hf : LowerSemicontinuousAt f y)
    (hg : ContinuousAt g x) (hy : g x = y) : LowerSemicontinuousAt (fun x ↦ f (g x)) x :=
  by
  rw [← hy] at hf
  exact comp_continuousAt hf hg

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