lowerSemicontinuous_indicator — Mathlib

English

If s is closed and y ≤ 0, then the function indicator_s·y is lower semicontinuous.

Русский

Если s замкнуто и y ≤ 0, то функция индикатора s умноженная на y—нижнеполупреграммна (low semicontinuous).

LaTeX

$$$s\ ext{IsClosed},\; y \le 0 \Rightarrow \operatorname{LowerSemicontinuous}(\mathbf{1}_s \cdot y).$$$

Lean4

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

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