equivWithAbs_image_mem_nhds_zero — Mathlib

English

Under equivalence, the image of nhds zero by the equivalence is nhds zero.

Русский

При эквивалентности образ nhds нуля по эквивалентности совпадает с nhds нуля.

LaTeX

$$$ (v IsEquiv w) \Rightarrow WithAbs.equivWithAbs v w '' 𝓝 0 \subset 𝓝 0 $$$

Lean4

theorem equivWithAbs_image_mem_nhds_zero (h : v.IsEquiv w) {U : Set (WithAbs v)} (hU : U ∈ 𝓝 0) :
    WithAbs.equivWithAbs v w '' U ∈ 𝓝 0 := by
  rw [Metric.mem_nhds_iff] at hU ⊢
  obtain ⟨ε, hε, hU⟩ := hU
  obtain ⟨c, hc, hvw⟩ := isEquiv_iff_exists_rpow_eq.1 h
  refine ⟨ε ^ c, rpow_pos_of_pos hε _, fun x hx ↦ ?_⟩
  rw [← RingEquiv.apply_symm_apply (WithAbs.equivWithAbs v w) x]
  refine Set.mem_image_of_mem _ (hU ?_)
  rw [Metric.mem_ball, dist_zero_right, WithAbs.norm_eq_abv, ← funext_iff.1 hvw,
    rpow_lt_rpow_iff (v.nonneg _) hε.le hc] at hx
  simpa [WithAbs.norm_eq_abv]

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