comp_continuousAt — Mathlib

English

For UpperSemicontinuousAt f at x and ContinuousAt g at x, the composition f ∘ g is upper semicontinuous at x.

Русский

При наличии верхней полупрерывности f в точке x и непрерывности g в x, композиция f ∘ g имеет верхнюю полупрерывность в x.

LaTeX

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

Lean4

theorem comp_continuousAt {f : α → β} {g : ι → α} {x : ι} (hf : UpperSemicontinuousAt f (g x)) (hg : ContinuousAt g x) :
    UpperSemicontinuousAt (fun x ↦ f (g x)) x := fun _ lt ↦ hg.eventually (hf _ lt)

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