tendsto_Ico_Ioi_Ioi — Mathlib

English

There is a TendstoIxxClass instance for Ico on principal (Ioi a) mapping to itself.

Русский

Существует экземпляр TendstoIxxClass для Ico на principal (Ioi a) отображающийся в саму себя.

LaTeX

$$$\\forall a:\\alpha,\\ TendstoIxxClass Ico (\\mathrm{principal}(\\mathrm{Ioi}(a))) (\\mathrm{principal}(\\mathrm{Ioi}(a)))$$$

Lean4

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

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