mono

Mathlib.Topology.Semicontinuous

URI: https://scilib.ai/kg/mathlib#LowerSemicontinuousWithinAt.mono

← MathLib Explorer

English

If h is lower semicontinuous within s and t ⊆ s, then h is lower semicontinuous within t.

Русский

Если h-LSC в рамках s, и t ⊆ s, то h-LSC в рамках t.

LaTeX

$$LowerSemicontinuousWithinAt f s x → t ⊆ s → LowerSemicontinuousWithinAt f t x$$

Lean4

theorem mono (h : LowerSemicontinuousWithinAt f s x) (hst : t ⊆ s) : LowerSemicontinuousWithinAt f t x := fun y hy =>
  Filter.Eventually.filter_mono (nhdsWithin_mono _ hst) (h y hy)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru