tendsto_Icc_pure_pure — Mathlib

English

For a, in a linear order, the interval Icc(a) with the pure construction converges to itself, reflecting the connectedness of the interval under the pure construction.

Русский

Для линейного порядка и интервала Icc(a) с чистой (pure) конструкцией существует схождение к самому себе, отображающее связность интервала под чистой конструкцией.

LaTeX

$$$$ \operatorname{TendstoIxxClass}(Icc, \mathrm{pure}(a), \mathrm{pure}(a)) $$$$

Lean4

instance tendsto_Icc_pure_pure {a : α} : TendstoIxxClass Icc (pure a) (pure a : Filter α) :=
  by
  rw [← principal_singleton]
  exact tendstoIxxClass_principal.2 ordConnected_singleton.out

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