isUniformInducing_toLp — Mathlib

English

Another form of the uniform-inducing property for toLp, under the same hypotheses.

Русский

Ещё одно выражение свойства равномерного индуцирования для toLp, при тех же предпосылках.

LaTeX

$$IsUniformInducing (@toLp p (Π i, β i))$$

Lean4

theorem isUniformInducing_toLp [∀ i, PseudoEMetricSpace (β i)] : IsUniformInducing (@toLp p (Π i, β i)) :=
  (antilipschitzWith_toLp p β).isUniformInducing (lipschitzWith_toLp p β).uniformContinuous

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