uniformContinuous_inr

Mathlib.Topology.Instances.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.uniformContinuous_inr

English

The embedding inr: M → tsze R M is uniformly continuous (assuming Zero R).

Русский

Встраивание inr: M → tsze R M является равномерно непрерывным (при нуле в R).

LaTeX

$$$\\operatorname{UniformContinuous}(\\mathrm{inr}: M \\to \\mathrm{tsze}(R,M))$$$

Lean4

theorem uniformContinuous_inr [Zero R] : UniformContinuous (inr : M → tsze R M) :=
  uniformContinuous_const.prodMk uniformContinuous_id

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

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

Разделы

Аффилиация

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