tendstoIcoClassNhds — Mathlib

English

An instance asserts TendstoIxxClass for Icc around nhds a in an OrderTopology space.

Русский

Экземпляр утверждает TendstoIxxClass для Icc вокруг nhds a в пространстве с OrderTopology.

LaTeX

$$$\\text{instance }\\text{tendstoIccClassNhds }[OrderTopology\\ α](a) : \\text{TendstoIxxClass } Icc (nhds(a)) (nhds(a))$$$

Lean4

instance tendstoIcoClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ico (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

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