isUniformEmbedding_pureCauchy — Mathlib

English

The map pureCauchy: α → CauchyFilter α is a uniform embedding (hence an embedding with respect to the uniform structures).

Русский

Функция pureCauchy: α → CauchyFilter α является равномерным вложением.

LaTeX

$$$\\text{IsUniformEmbedding}(\\text{pureCauchy})$$$

Lean4

theorem isUniformEmbedding_pureCauchy : IsUniformEmbedding (pureCauchy : α → CauchyFilter α)
    where
  __ := isUniformInducing_pureCauchy
  injective _a₁ _a₂ h := pure_injective <| Subtype.ext_iff.1 h

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