lowerSemicontinuousWithinAt_iff_le_liminf

English

LowerSemicontinuousWithinAt f s x is characterized by f(x) ≤ liminf f along nhdsWithin(x, s).

Русский

LowerSemicontinuousWithinAt f s x характеризуется не выше чем liminf f вдоль nhdsWithin(x, s).

LaTeX

$$$\text{LowerSemicontinuousWithinAt}(f, s, x) \iff f(x) \le \liminf f(\mathcal{N}_{x}^{s})$$$

Lean4

theorem lowerSemicontinuousWithinAt_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x) :=
  by
  constructor
  · intro hf; unfold LowerSemicontinuousWithinAt at hf
    contrapose! hf
    obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi; use y
    exact
      ⟨ylt, fun h =>
        ltz.not_ge
          (le_liminf_of_le (by isBoundedDefault) (h.mono fun _ h₂ => le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))⟩
  exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

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