tendstoIocClassNhds

Mathlib.Topology.Order.Basic

URI: https://scilib.ai/kg/mathlib#tendstoIocClassNhds

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\\text{TendstoIxxClass } Ioc (nhds(a)) (nhds(a))$$$

Lean4

instance tendstoIocClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioc (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru