mono

Mathlib.Topology.Semicontinuous

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

English

If f is upper semicontinuous on s and t ⊆ s, then f is upper semicontinuous on t.

Русский

Если f верхнеполупрерывна на s и t ⊆ s, то на t тоже.

LaTeX

$$$\\displaystyle \\text{UpperSemicontinuousOn}(f,s) \\land t\\subseteq s \\Rightarrow \\text{UpperSemicontinuousOn}(f,t)$$$

Lean4

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

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

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

Разделы

Аффилиация

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