isUniformEmbedding_subtypeEmb — Mathlib

English

Given a predicate p on α and an embedding e, the induced subtype embedding preserves uniform embedding.

Русский

При заданном предикате p на α и вложении e, индуцированное вложение подтипа сохраняет равномерное вложение.

LaTeX

$$$\\text{IsUniformEmbedding}(\\text{IsDenseEmbedding.subtypeEmb } p\ x\ e)$$$

Lean4

theorem isUniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : IsUniformEmbedding e) (de : IsDenseEmbedding e) :
    IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
  { comap_uniformity := by
      simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype, ue.comap_uniformity.symm]
    injective := (de.subtype p).injective }

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