mono

Mathlib.Topology.Semicontinuous

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

English

Mono-lemma for LowerSemicontinuousOn regarding subset inclusion.

Русский

Моно-лемма для LowerSemicontinuousOn по включению подмножеств.

LaTeX

$$LowerSemicontinuousOn f s → t ⊆ s → LowerSemicontinuousOn f t$$

Lean4

theorem mono (h : LowerSemicontinuousOn f s) (hst : t ⊆ s) : LowerSemicontinuousOn f t := fun x hx =>
  (h x (hst hx)).mono hst

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

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

Разделы

Аффилиация

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