tendsto_Ioc_uIcc_uIcc — Mathlib

English

Let α be a linear order. The Tendsto property Ioc with p uch of uIcc also holds, indicating convergence from Ioc to Icc-like constructs under uIcc.

Русский

Пусть α — линейный порядок. Свойство Tendsto для Ioc и uIcc сохраняется, указывая на схождение из Ioc в конструкции, подобные Icc при uIcc.

LaTeX

$$$$ \operatorname{TendstoIxxClass}(Ioc, \mathrm{principal}(\mathrm{Set.uIcc}(a,b)), \mathrm{principal}(\mathrm{Set.uIcc}(a,b))) $$$$

Lean4

instance tendsto_Ioc_uIcc_uIcc {a b : α} : TendstoIxxClass Ioc (𝓟 [[a, b]]) (𝓟 [[a, b]]) :=
  Filter.tendsto_Ioc_Icc_Icc

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