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 }