comp_lowerSemicontinuousWithinAt_antitone

English

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

Русский

Если g непрерывна в f(x) и f ниже полупрерывна на s в x, а g антитонна, то g∘f верхне полупрерывна на s в x.

LaTeX

$$$\\text{ContinuousAt } g (f x) \\land \\text{LowerSemicontinuousWithinAt } f s x \\land \\text{Antitone } g \\Rightarrow \\text{UpperSemicontinuousWithinAt } (g∘f) s x$$$

Lean4

theorem comp_lowerSemicontinuousWithinAt_antitone {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : LowerSemicontinuousWithinAt f s x) (gmon : Antitone g) : UpperSemicontinuousWithinAt (g ∘ f) s x :=
  @ContinuousAt.comp_lowerSemicontinuousWithinAt α _ x s γ _ _ _ δᵒᵈ _ _ _ g f hg hf gmon

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