lowerSemicontinuous_indicator — Mathlib

English

If s is open and y ≥ 0, then the indicator function of s with value y is lower semicontinuous.

Русский

Если s открыто, и y неотрицательно, то индикаторная функция s принимает значение y на s и является нижней полупрерывной.

LaTeX

$$$\operatorname{LowerSemicontinuous}(\mathbf{1}_{s} \cdot y) \quad (s\text{ open},\ y\ge 0)$$$

Lean4

theorem lowerSemicontinuous_indicator (hs : IsOpen s) (hy : 0 ≤ y) : LowerSemicontinuous (indicator s fun _x => y) :=
  by
  intro x z hz
  by_cases h : x ∈ s <;> simp [h] at hz
  · filter_upwards [hs.mem_nhds h]
    simp +contextual [hz]
  · refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

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