comp_upperSemicontinuousOn_antitone

English

If hg: ContinuousAt g (f x) and hf: UpperSemicontinuousAt f x, and gmon: Monotone g, then UpperSemicontinuousWithinAt (g ∘ f) s x.

Русский

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

LaTeX

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

Lean4

theorem comp_upperSemicontinuousOn_antitone {g : γ → δ} {f : α → γ} (hg : Continuous g) (hf : UpperSemicontinuousOn f s)
    (gmon : Antitone g) : LowerSemicontinuousOn (g ∘ f) s := fun x hx =>
  hg.continuousAt.comp_upperSemicontinuousWithinAt_antitone (hf x hx) gmon

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