case h.e'_6
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ ball p x r = {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (↑p ∘ fun z => z + -x) x_1 < r}
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (ball p x r)
convert (p.convexOn.translate_left (-x)).convex_lt r
case h.e'_6.h
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ ball p x r ↔ y ∈ {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (↑p ∘ fun z => z + -x) x_1 < r}
case h.e'_6
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ ball p x r = {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (↑p ∘ fun z => z + -x) x_1 < r}
ext y
case h.e'_6.h
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ ↑p (y + -x) < r ↔ y ∈ {x_1 | (↑p ∘ fun z => z + -x) x_1 < r}
case h.e'_6.h
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ ball p x r ↔ y ∈ {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (↑p ∘ fun z => z + -x) x_1 < r}
rw [preimage_univ, sep_univ, p.mem_ball, sub_eq_add_neg]
no goals
case h.e'_6.h
R : Type ?u.1306084
R' : Type ?u.1306087
𝕜 : Type u_2
𝕜₂ : Type ?u.1306093
𝕜₃ : Type ?u.1306096
𝕝 : Type ?u.1306099
E : Type u_1
E₂ : Type ?u.1306105
E₃ : Type ?u.1306108
F : Type ?u.1306111
G : Type ?u.1306114
ι : Type ?u.1306117
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ ↑p (y + -x) < r ↔ y ∈ {x_1 | (↑p ∘ fun z => z + -x) x_1 < r}
rfl