case h
R : Type ?u.1006960
R' : Type ?u.1006963
𝕜 : Type u_2
𝕜₂ : Type ?u.1006969
𝕜₃ : Type ?u.1006972
𝕝 : Type ?u.1006975
E : Type u_1
E₂ : Type ?u.1006981
E₃ : Type ?u.1006984
F : Type ?u.1006987
G : Type ?u.1006990
ι : Type ?u.1006993
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ↑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | ↑p x < r}
R : Type ?u.1006960
R' : Type ?u.1006963
𝕜 : Type u_2
𝕜₂ : Type ?u.1006969
𝕜₃ : Type ?u.1006972
𝕝 : Type ?u.1006975
E : Type u_1
E₂ : Type ?u.1006981
E₃ : Type ?u.1006984
F : Type ?u.1006987
G : Type ?u.1006990
ι : Type ?u.1006993
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
⊢ ↑p ⁻¹' Metric.ball 0 r = {x | ↑p x < r}
ext x
no goals
case h
R : Type ?u.1006960
R' : Type ?u.1006963
𝕜 : Type u_2
𝕜₂ : Type ?u.1006969
𝕜₃ : Type ?u.1006972
𝕝 : Type ?u.1006975
E : Type u_1
E₂ : Type ?u.1006981
E₃ : Type ?u.1006984
F : Type ?u.1006987
G : Type ?u.1006990
ι : Type ?u.1006993
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ↑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | ↑p x < r}
simp only [mem_setOf, mem_preimage, mem_ball_zero_iff, Real.norm_of_nonneg (map_nonneg p _)]