uniformContinuous_inl — Mathlib

English

The embedding inl: R → tsze R M is uniformly continuous (assuming M has a zero element).

Русский

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

LaTeX

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

Lean4

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

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