case h
R : Type ?u.1012446
R' : Type ?u.1012449
𝕜 : Type u_2
𝕜₂ : Type ?u.1012455
𝕜₃ : Type ?u.1012458
𝕝 : Type ?u.1012461
E : Type u_1
E₂ : Type ?u.1012467
E₃ : Type ?u.1012470
F : Type ?u.1012473
G : Type ?u.1012476
ι : Type ?u.1012479
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.closedBall 0 r ↔ x ∈ {x | ↑p x ≤ r}
R : Type ?u.1012446
R' : Type ?u.1012449
𝕜 : Type u_2
𝕜₂ : Type ?u.1012455
𝕜₃ : Type ?u.1012458
𝕝 : Type ?u.1012461
E : Type u_1
E₂ : Type ?u.1012467
E₃ : Type ?u.1012470
F : Type ?u.1012473
G : Type ?u.1012476
ι : Type ?u.1012479
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
⊢ ↑p ⁻¹' Metric.closedBall 0 r = {x | ↑p x ≤ r}
ext x
no goals
case h
R : Type ?u.1012446
R' : Type ?u.1012449
𝕜 : Type u_2
𝕜₂ : Type ?u.1012455
𝕜₃ : Type ?u.1012458
𝕝 : Type ?u.1012461
E : Type u_1
E₂ : Type ?u.1012467
E₃ : Type ?u.1012470
F : Type ?u.1012473
G : Type ?u.1012476
ι : Type ?u.1012479
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.closedBall 0 r ↔ x ∈ {x | ↑p x ≤ r}
simp only [mem_setOf, mem_preimage, mem_closedBall_zero_iff,
  Real.norm_of_nonneg (map_nonneg p _)]