English
If v is equivalent to w, then the induced map on WithAbs is an embedding.
Русский
Если v эквивалентно w, то индуцированная карта на WithAbs является вложением.
LaTeX
$$$ (v IsEquiv w) \Rightarrow IsEmbedding (WithAbs.equivWithAbs v w)$$$
Lean4
theorem isEmbedding_equivWithAbs (h : v.IsEquiv w) : IsEmbedding (WithAbs.equivWithAbs v w) :=
by
refine IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦ ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩
·
exact
⟨WithAbs.equivWithAbs v w '' U, h.equivWithAbs_image_mem_nhds_zero hU, by
simp [RingEquiv.image_eq_preimage, Set.preimage_preimage]⟩
· rw [← RingEquiv.coe_toEquiv, ← Filter.map_equiv_symm] at hU
obtain ⟨s, hs, hss⟩ := Filter.mem_map_iff_exists_image.1 hU
rw [← RingEquiv.coe_toEquiv_symm, WithAbs.equivWithAbs_symm] at hss
exact Filter.mem_of_superset (h.symm.equivWithAbs_image_mem_nhds_zero hs) hss
