tendsto_Ico_Ici_Ici

Mathlib.Order.Filter.Interval

URI: https://scilib.ai/kg/mathlib#Filter.tendsto_Ico_Ici_Ici

English

For any a, TendstoIxxClass Ico (principal (Ici a)) (principal (Ici a)).

Русский

Для любого a выполнено TendstoIxxClass Ico (principal (Ici a)) (principal (Ici a)).

LaTeX

$$$\\forall a:\\alpha,\\ TendstoIxxClass Ico (\\mathcal{P}(\\mathrm{Icc}(a))) (\\mathcal{P}(\\mathrm{Icc}(a)))$$$

Lean4

instance tendsto_Ico_Ici_Ici {a : α} : TendstoIxxClass Ico (𝓟 (Ici a)) (𝓟 (Ici a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

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

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

Разделы

Аффилиация

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