comp_upperSemicontinuousWithinAt_antitone

English

If hg: ContinuousAt g (f x), hf: UpperSemicontinuousWithinAt f s x, and gmon: Antitone g, then g∘f is lower semicontinuousWithinAt at x.

Русский

Если hg: непрерывна g в f(x), hf: верхняя полупрерывность функции 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_upperSemicontinuousWithinAt_antitone {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : UpperSemicontinuousWithinAt f s x) (gmon : Antitone g) : LowerSemicontinuousWithinAt (g ∘ f) s x :=
  @ContinuousAt.comp_upperSemicontinuousWithinAt α _ x s γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon

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