star

Mathlib.Topology.Algebra.Star

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

English

If f is continuously defined on s, then star(f) is continuously defined on s.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem star (hf : ContinuousOn f s) : ContinuousOn (fun x => star (f x)) s :=
  continuous_star.comp_continuousOn hf

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

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

Разделы

Аффилиация

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