K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ∀ (x : K), ContinuousAt (↑v) x
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ Continuous ↑v
rw [continuous_iff_continuousAt]
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
⊢ ContinuousAt (↑v) x
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ∀ (x : K), ContinuousAt (↑v) x
intro x
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ContinuousAt (↑v) 0

case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
⊢ ContinuousAt (↑v) x
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
⊢ ContinuousAt (↑v) x
rcases eq_or_ne x 0 with (rfl | h)
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, ↑v x < γ₀
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ContinuousAt (↑v) 0
rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ ∀ᶠ (x : K) in 𝓝 0, ↑v x < γ
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
⊢ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, ↑v x < γ₀
intro γ hγ
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ γ_1, {x | ↑v x < ↑γ_1} ⊆ {x | ↑v x < γ}
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ ∀ᶠ (x : K) in 𝓝 0, ↑v x < γ
rw [Filter.Eventually, Valued.mem_nhds_zero]
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ {x | ↑v x < ↑(Units.mk0 γ hγ)} ⊆ {x | ↑v x < γ}
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ γ_1, {x | ↑v x < ↑γ_1} ⊆ {x | ↑v x < γ}
use Units.mk0 γ hγ
no goals
case inl
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ {x | ↑v x < ↑(Units.mk0 γ hγ)} ⊆ {x | ↑v x < γ}
rfl
case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : ↑v x ≠ 0
⊢ ContinuousAt (↑v) x
case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
⊢ ContinuousAt (↑v) x
have v_ne : (v x : Γ₀) ≠ 0 := (Valuation.ne_zero_iff _).mpr h
case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : ↑v x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, ↑v x_1 = ↑v x
case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : ↑v x ≠ 0
⊢ ContinuousAt (↑v) x
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
no goals
case inr
K : Type u_2
inst✝² : DivisionRing K
Γ₀ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : ↑v x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, ↑v x_1 = ↑v x
apply Valued.loc_const v_ne