English
Two equivalent real absolute values induce a homeomorph on the underlying structure.
Русский
Два эквивалентных вещественных абсолютных значения порождают гомеоморфизм на базовой структуре.
LaTeX
$$$ v.IsEquiv w \Rightarrow IsHomeomorph (WithAbs.equivWithAbs v w)$$$
Lean4
theorem isEquiv_iff_isHomeomorph (v w : AbsoluteValue F ℝ) : v.IsEquiv w ↔ IsHomeomorph (WithAbs.equivWithAbs v w) :=
by
rw [isHomeomorph_iff_isEmbedding_surjective]
refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩
refine isEquiv_iff_lt_one_iff.2 fun x ↦ ?_
conv_lhs => rw [← (WithAbs.equiv v).apply_symm_apply x]
conv_rhs => rw [← (WithAbs.equiv w).apply_symm_apply x]
simp_rw [← WithAbs.norm_eq_abv, ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]
exact
⟨fun h ↦ by simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h, fun h ↦ by
simpa [Function.comp_def] using
(hi.continuous_iff (f := (WithAbs.equivWithAbs v w).symm)).2 continuous_id |>.tendsto 0 |>.comp h⟩
