lowerSemicontinuousWithinAt — Mathlib

English

If f is lower semicontinuous, then f is lower semicontinuous within any subset s at any point x.

Русский

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

LaTeX

$$$\operatorname{LowerSemicontinuousWithinAt}(f, s, x)$$$

Lean4

theorem lowerSemicontinuousWithinAt (h : LowerSemicontinuous f) (s : Set α) (x : α) :
    LowerSemicontinuousWithinAt f s x :=
  (h x).lowerSemicontinuousWithinAt s

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