tendstoIooClassNhds

Mathlib.Topology.Order.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

instance tendstoIooClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

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

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

Разделы

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

Аффилиация

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