tendstoIccClassNhds — Mathlib

English

There is a TendstoIxxClass structure for Icc with respect to nhds a under OrderTopology α.

Русский

Существует структура TendstoIxxClass для Icc относительно nhds a в OrderTopology α.

LaTeX

$$$\\text{TendstoIxxClass }\\mathrm{Set.Icc} \\ (nhds(a))\\ (nhds(a))$$$

Lean4

instance tendstoIccClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Icc (𝓝 a) (𝓝 a) :=
  by
  simp only [nhds_eq_order, iInf_subtype']
  refine ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass fun s _ => ?_
  refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out <;> intro _ _
  exacts [ordConnected_Ioi, ordConnected_Iio]

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