tendsto_fst

Mathlib.Order.Filter.Prod

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

English

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

Русский

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

LaTeX

$$$$\\operatorname{Tendsto}\\,\\operatorname{fst}\\ (f \\times g)\; f.$$$

Lean4

theorem tendsto_fst : Tendsto Prod.fst (f ×ˢ g) f :=
  tendsto_inf_left tendsto_comap

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

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

Разделы

Аффилиация

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