star

Mathlib.Topology.Algebra.Star

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

English

If f is continuous, then x ↦ star(f(x)) is continuous.

Русский

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

LaTeX

$$$\mathrm{Continuous}\bigl( f \bigr) \Rightarrow \mathrm{Continuous}\bigl( \lambda x. \mathrm{star}(f(x)) \bigr)$$$

Lean4

@[continuity, fun_prop]
theorem star (hf : Continuous f) : Continuous fun x => star (f x) :=
  continuous_star.comp hf

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

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

Разделы

Аффилиация

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