case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.50113
𝕝 : Type ?u.50116
𝕝₂ : Type ?u.50119
E : Type u_1
F : Type ?u.50125
G : Type ?u.50128
ι : Type u_3
ι' : Type ?u.50134
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ basisSets p
s : Finset ι
r : ℝ
w✝ : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V ⊆ (fun x => -x) ⁻¹' U
𝕜 : Type u_2
𝕜₂ : Type ?u.50113
𝕝 : Type ?u.50116
𝕝₂ : Type ?u.50119
E : Type u_1
F : Type ?u.50125
G : Type ?u.50128
ι : Type u_3
ι' : Type ?u.50134
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ basisSets p
⊢ ∃ V, V ∈ basisSets p ∧ V ⊆ (fun x => -x) ⁻¹' U
rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.50113
𝕝 : Type ?u.50116
𝕝₂ : Type ?u.50119
E : Type u_1
F : Type ?u.50125
G : Type ?u.50128
ι : Type u_3
ι' : Type ?u.50134
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ basisSets p
s : Finset ι
r : ℝ
w✝ : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V ⊆ ball (Finset.sup s p) 0 r
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.50113
𝕝 : Type ?u.50116
𝕝₂ : Type ?u.50119
E : Type u_1
F : Type ?u.50125
G : Type ?u.50128
ι : Type u_3
ι' : Type ?u.50134
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ basisSets p
s : Finset ι
r : ℝ
w✝ : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V ⊆ (fun x => -x) ⁻¹' U
rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]
no goals
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.50113
𝕝 : Type ?u.50116
𝕝₂ : Type ?u.50119
E : Type u_1
F : Type ?u.50125
G : Type ?u.50128
ι : Type u_3
ι' : Type ?u.50134
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU' : U ∈ basisSets p
s : Finset ι
r : ℝ
w✝ : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V ⊆ ball (Finset.sup s p) 0 r
exact ⟨U, hU', Eq.subset hU⟩