English
Given de : IsDenseEmbedding e, the subtype embedding using p yields IsDenseEmbedding.
Русский
Для данного de : IsDenseEmbedding e отображение подмножества даёт плотное вложение.
LaTeX
$$$IsDenseEmbedding (subtypeEmb p e)$$$
Lean4
protected theorem subtype (de : IsDenseEmbedding e) (p : α → Prop) : IsDenseEmbedding (subtypeEmb p e)
where
dense :=
dense_iff_closure_eq.2 <| by
ext ⟨x, hx⟩
rw [image_eq_range] at hx
simpa [closure_subtype, ← range_comp, (· ∘ ·)]
injective := (de.injective.comp Subtype.coe_injective).codRestrict _
eq_induced :=
(induced_iff_nhds_eq _).2 fun ⟨x, hx⟩ => by
simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap, Function.comp_def]
