tendsto_diag

Mathlib.Order.Filter.Prod

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

English

The diagonal embedding i ↦ (i,i) is a Tendsto from f to f ×ˢ f: Tendsto (fun i => (i,i)) f (f ×ˢ f).

Русский

Диагональная вложение i ↦ (i,i) есть предел: Tendsto (i,i) подаётся от f к f × f.

LaTeX

$$$$\operatorname{Tendsto}(\lambda i. (i,i))\; f\; (f \times f).$$$$

Lean4

theorem tendsto_diag : Tendsto (fun i => (i, i)) f (f ×ˢ f) :=
  tendsto_iff_eventually.mpr fun _ hpr => hpr.diag_of_prod

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

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

Разделы

Аффилиация

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