comp_lowerSemicontinuousAt_antitone

English

Let f: α → γ, s: Set α. Then LowerSemicontinuousOn f s is equivalent to epigraph being closed, under appropriate hypotheses on γ.

Русский

Пусть f: α → γ, s ⊆ α. ТогдаLowerSemicontinuousOn f s эквивалентна тому, что эпиграф замкнут при подходящих гипотезах на γ.

LaTeX

$$$\\text{LowerSemicontinuousOn } f s \\iff \\text{IsClosed }\\{ p=(x,t) \\mid x∈s ∧ f(x) ≤ t \\}$$$

Lean4

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

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