continuous_extend — Mathlib

English

If f is an IsUniformInducing map, then the extension pkg.extend f is also IsUniformInducing.

Русский

Если f — отображение с индукцией по униформности, то его продолжение также индукционно по униформности.

LaTeX

$$$IsUniformInducing(f) \\Rightarrow IsUniformInducing(pkg.extend f)$$$

Lean4

theorem continuous_extend : Continuous (pkg.extend f) :=
  pkg.uniformContinuous_extend.continuous

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