upperSemicontinuous_indicator — Mathlib

English

If s is open and y ≤ 0, the indicator function of s with value y is upper semicontinuous.

Русский

Если s открыто, и y ≤ 0, индикаторная функция χ_s(y) верхнеполупрерывна.

LaTeX

$$$\\mathrm{IsOpen}(s) \\land y \\le 0 \\Rightarrow \\mathrm{UpperSemicontinuous}(\\mathrm{indicator}(s, \\lambda x. y))$$$

Lean4

theorem upperSemicontinuous_indicator (hs : IsOpen s) (hy : y ≤ 0) : UpperSemicontinuous (indicator s fun _x => y) :=
  @IsOpen.lowerSemicontinuous_indicator α _ βᵒᵈ _ s y _ hs hy

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