exists

Mathlib.Topology.Algebra.InfiniteSum.UniformOn

URI: https://scilib.ai/kg/mathlib#MultipliableUniformlyOn.exists

English

As above, there exists a g with HasProdUniformlyOn f g 𝔖.

Русский

Как выше, существует g такая, что HasProdUniformlyOn f g 𝔖.

LaTeX

$$$\\exists g\\; HasProdUniformlyOn f\\ g\\ 𝔖$$$

Lean4

@[to_additive]
theorem «exists» (h : MultipliableUniformlyOn f 𝔖) : ∃ g, HasProdUniformlyOn f g 𝔖 :=
  h

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

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

Разделы

Аффилиация

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