upperSemicontinuous_indicator — Mathlib

English

If s is closed and y ≥ 0, then χ_s(y) is upper semicontinuous.

Русский

Если s замкнуто и y ≥ 0, χ_s(y) верхнеполупрерывна.

LaTeX

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

Lean4

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

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