tendsto_star

Mathlib.Topology.Algebra.Star

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

English

The star operation preserves limits along a net (tends to star of the limit).

Русский

Операция звезды сохраняет пределы по сети: tendsto star(f) к star(lim).

LaTeX

$$$\text{Tendsto}(\mathrm{star} \circ f, l, \mathrm{nhds}(\mathrm{star}(a)))$$$

Lean4

theorem tendsto_star (a : R) : Tendsto star (𝓝 a) (𝓝 (star a)) :=
  continuousAt_star

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

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

Разделы

Аффилиация

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