case h
R : Type ?u.950251
R' : Type ?u.950254
𝕜 : Type u_3
𝕜₂ : Type u_1
𝕜₃ : Type ?u.950263
𝕝 : Type ?u.950266
E : Type u_4
E₂ : Type u_2
E₃ : Type ?u.950275
F : Type ?u.950278
G : Type ?u.950281
ι : Type ?u.950284
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ closedBall (comp p f) x r ↔ x✝ ∈ ↑f ⁻¹' closedBall p (↑f x) r
R : Type ?u.950251
R' : Type ?u.950254
𝕜 : Type u_3
𝕜₂ : Type u_1
𝕜₃ : Type ?u.950263
𝕝 : Type ?u.950266
E : Type u_4
E₂ : Type u_2
E₃ : Type ?u.950275
F : Type ?u.950278
G : Type ?u.950281
ι : Type ?u.950284
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
⊢ closedBall (comp p f) x r = ↑f ⁻¹' closedBall p (↑f x) r
ext
no goals
case h
R : Type ?u.950251
R' : Type ?u.950254
𝕜 : Type u_3
𝕜₂ : Type u_1
𝕜₃ : Type ?u.950263
𝕝 : Type ?u.950266
E : Type u_4
E₂ : Type u_2
E₃ : Type ?u.950275
F : Type ?u.950278
G : Type ?u.950281
ι : Type ?u.950284
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ closedBall (comp p f) x r ↔ x✝ ∈ ↑f ⁻¹' closedBall p (↑f x) r
simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]