tendsto_atBot_diagonal — Mathlib

English

The map a ↦ (a,a) tends to atBot in α given α is a Preorder.

Русский

Отображение a ↦ (a,a) стремится к atBot в α, если α упорядочено.

LaTeX

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

Lean4

theorem tendsto_atBot_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atBot atBot :=
  by
  rw [← prod_atBot_atBot_eq]
  exact tendsto_id.prodMk tendsto_id

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