tendsto_snd

Mathlib.Order.Filter.Prod

URI: https://scilib.ai/kg/mathlib#Filter.tendsto_snd

English

The second projection map from the product to the second coordinate preserves limits: Tendsto Prod.snd (f × g) g.

Русский

Вторая проекция из произведения в вторую координату сохраняет пределы: Tendsto Prod.snd (f × g) g.

LaTeX

$$$$\operatorname{Tendsto} \ \operatorname{snd} (f \times g)\ g.$$$

Lean4

theorem tendsto_snd : Tendsto Prod.snd (f ×ˢ g) g :=
  tendsto_inf_right tendsto_comap

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

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

Разделы

Аффилиация

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