comp_continuousAt_of_eq — Mathlib

English

If f is upper semicontinuous at y, g is continuous at x, and gx = y, then f∘g is upper semicontinuous at x.

Русский

Если f имеет верхнюю полупрерывность в y, g непрерывна в x, и g(x)=y, то f∘g имеет верхнюю полупрерывность в x.

LaTeX

$$$hf : UpperSemicontinuousAt f y,\\ hg : ContinuousAt g x,\\ hy : g x = y\\Rightarrow\\; \\text{UpperSemicontinuousAt } (f \\circ g) x$$$

Lean4

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

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