comp_upperSemicontinuousAt — Mathlib

English

If g is continuous at f(x), f is upper semicontinuous within s at x, and g is antitone, then g∘f is lower semicontinuous within s at x.

Русский

Если g непрерывна в f(x), f имеет верхнюю полупрерывность внутри s в x, а g антипотентна, то композиция g∘f имеет нижнюю полупрерывность внутри s в x.

LaTeX

$$$hg : ContinuousAt g (f x),\\ hf : UpperSemicontinuousWithinAt f s x,\\ gmon : Antitone g\\Rightarrow\\; \\text{LowerSemicontinuousWithinAt } (g \\circ f) s x$$$

Lean4

theorem comp_upperSemicontinuousAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x)) (hf : UpperSemicontinuousAt f x)
    (gmon : Monotone g) : UpperSemicontinuousAt (g ∘ f) x :=
  @ContinuousAt.comp_lowerSemicontinuousAt α _ x γᵒᵈ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon.dual

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