lowerSemicontinuousOn — Mathlib

English

If f is lower semicontinuous, then f is lower semicontinuous on any subset s.

Русский

Если f — нижняя полупрерывная, то она имеет нижнюю полупрерывность на любом подмножестве s.

LaTeX

$$$\operatorname{LowerSemicontinuousOn}(f, s)$$$

Lean4

theorem lowerSemicontinuousOn (h : LowerSemicontinuous f) (s : Set α) : LowerSemicontinuousOn f s := fun x _hx =>
  h.lowerSemicontinuousWithinAt s x

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