English
Let p ≥ 1 and α, β be pseudo-metric spaces. The canonical map from α × β into the Lp-space associated to α × β is uniform inducing; in other words, the uniform structure on α × β is induced by its image under the toLp construction.
Русский
Пусть p ≥ 1, а и β — псевдометрические пространства. Каноническое отображение из α × β в пространство Lp, связанное с α × β, является равномерно индуцирующим; то есть равномерная структура α × β является индукцией по изображению с помощью отображения toLp.
LaTeX
$$$\mathrm{IsUniformInducing}(\mathrm{toLp}_p(\alpha \times \beta))$$$
Lean4
theorem isUniformInducing_toLp [PseudoEMetricSpace α] [PseudoEMetricSpace β] : IsUniformInducing (@toLp p (α × β)) :=
(prod_antilipschitzWith_toLp p α β).isUniformInducing (prod_lipschitzWith_toLp p α β).uniformContinuous
