mono

Mathlib.Topology.ContinuousOn

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

English

If f is continuous on t and s ⊆ t, then f is continuous on s.

Русский

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

LaTeX

$$$h : ContinuousOn f t x \\land s \\subseteq t \\Rightarrow ContinuousOn f s x$$$

Lean4

theorem mono (h : ContinuousWithinAt f t x) (hs : s ⊆ t) : ContinuousWithinAt f s x :=
  h.mono_left (nhdsWithin_mono x hs)

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

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

Разделы

Аффилиация

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