comp_lowerSemicontinuousWithinAt — Mathlib

English

If s is closed and p ranges over pairs with x ∈ s and f(x) ≤ p2, the law characterizes local lower semicontinuity via epigraph being closed.

Русский

Если s замкнуто и рассматриваются пары (x,t) с x ∈ s и f(x) ≤ t, тогда локальная нижняя полупрерывность описывается замкнутость эпиграфа.

LaTeX

$$$\\text{LowerSemicontinuousOn} \\\\ f \\\\ s \\iff \\text{IsClosed} \\\\{ p=(x,t) : x∈s ∧ f(x) ≤ t \\}$ при условии замкнутости s.$$

Lean4

theorem comp_lowerSemicontinuousWithinAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : LowerSemicontinuousWithinAt f s x) (gmon : Monotone g) : LowerSemicontinuousWithinAt (g ∘ f) s x :=
  by
  intro y hy
  by_cases h : ∃ l, l < f x
  · obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y := exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h
    filter_upwards [hf z zlt] with a ha
    calc
      y < g (min (f x) (f a)) := hz (by simp [zlt, ha])
      _ ≤ g (f a) := gmon (min_le_right _ _)
  · simp only [not_exists, not_lt] at h
    exact Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))

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