tendsto_Ico_Iio_Iio — Mathlib

English

There is a TendstoIxxClass instance for Ico from principal (Iio a) to principal (Iio a).

Русский

Существует экземпляр TendstoIxxClass для Ico между principal(Iio a) и principal(Iio a).

LaTeX

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

Lean4

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

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