K : Type u_2
inst✝¹ : Field K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 (↑K x))) (𝓝 (↑v x))
K : Type u_2
inst✝¹ : Field K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ extension (↑K x) = ↑v x
refine' Completion.denseInducing_coe.extend_eq_of_tendsto _
K : Type u_2
inst✝¹ : Field K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (↑v) (𝓝 x) (𝓝 (↑v x))
K : Type u_2
inst✝¹ : Field K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (↑v) (Filter.comap (↑K) (𝓝 (↑K x))) (𝓝 (↑v x))
rw [← Completion.denseInducing_coe.nhds_eq_comap]
no goals
K : Type u_2
inst✝¹ : Field K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Tendsto (↑v) (𝓝 x) (𝓝 (↑v x))
exact Valued.continuous_valuation.continuousAt