isUniformInducing_extend — Mathlib

English

If f is an IsUniformInducing map, then the extended map pkg.extend f remains IsUniformInducing.

Русский

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

LaTeX

$$$\\text{IsUniformInducing}(f) \\Rightarrow \\text{IsUniformInducing}(pkg\\,.extend f)$$$

Lean4

theorem isUniformInducing_extend (h : IsUniformInducing f) : IsUniformInducing (pkg.extend f) :=
  by
  rw [extend_def _ h.uniformContinuous]
  exact pkg.isDenseInducing.isUniformInducing_extend pkg.isUniformInducing h

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