continuousWithinAt

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#Continuous.continuousWithinAt

English

If f is continuous, then it is continuous on any set s.

Русский

Если f непрерывна, то она непрерывна на любом множестве.

LaTeX

$$$$\text{Continuous}(f) \Rightarrow \text{ContinuousOn}(f,s).$$$$

Lean4

theorem continuousWithinAt (h : Continuous f) : ContinuousWithinAt f s x :=
  h.continuousAt.continuousWithinAt

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

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

Разделы

Аффилиация

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