star

Mathlib.Topology.Algebra.Star

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

English

If f is continuous within s at x, then star(f) is continuous within s at x.

Русский

Если f непрерывна внутри s в точке x, то star(f) непрерывна внутри s в x.

LaTeX

$$$\mathrm{ContinuousWithinAt}(\mathrm{star} \circ f, s, x)$$$

Lean4

theorem star (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => star (f x)) s x :=
  Filter.Tendsto.star hf

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

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

Разделы

Аффилиация

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