map_continuousWithinAt

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#map_continuousWithinAt

English

For f ∈ F and set s ⊆ α, f is ContinuousWithinAt on s at a for any a ∈ α.

Русский

Для f ∈ F и множества s ⊆ α функция f ограниченно непрерывна внутри s в точке a.

LaTeX

$$$\\text{map\_continuousWithinAt}(f,s,a) : \\text{ContinuousWithinAt } f\, s\, a.$$$

Lean4

theorem map_continuousWithinAt (f : F) (s : Set α) (a : α) : ContinuousWithinAt f s a :=
  (map_continuous f).continuousWithinAt

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

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

Разделы

Аффилиация

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