comp_upperSemicontinuousAt_antitone

English

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

Русский

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

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_antitone {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : UpperSemicontinuousAt f x) (gmon : Antitone g) : LowerSemicontinuousAt (g ∘ f) x :=
  @ContinuousAt.comp_upperSemicontinuousAt α _ x γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon

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