tendsto_atTop_diagonal — Mathlib

English

The diagonal map a ↦ (a,a) tends to atTop when domain tends to atTop.

Русский

Диагональное отображение a ↦ (a,a) стремится к atTop при стремлении области к atTop.

LaTeX

$$$\\operatorname{Tendsto}(\\lambda a: (a,a))\\, \\operatorname{atTop}\\, \\operatorname{atTop}$$$

Lean4

theorem tendsto_atTop_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atTop atTop :=
  by
  rw [← prod_atTop_atTop_eq]
  exact tendsto_id.prodMk tendsto_id

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