𝕜 : Type u_3
𝕜' : Type ?u.978
E : Type u_1
E' : Type ?u.984
F : Type ?u.987
ι : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V A
𝕜 : Type u_3
𝕜' : Type ?u.978
E : Type u_1
E' : Type ?u.984
F : Type ?u.987
ι : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
refine' ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => _⟩
case intro.intro
𝕜 : Type u_3
𝕜' : Type ?u.978
E : Type u_1
E' : Type ?u.984
F : Type ?u.987
ι : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A
𝕜 : Type u_3
𝕜' : Type ?u.978
E : Type u_1
E' : Type ?u.984
F : Type ?u.987
ι : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V A
rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩
no goals
case intro.intro
𝕜 : Type u_3
𝕜' : Type ?u.978
E : Type u_1
E' : Type ?u.984
F : Type ?u.987
ι : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A
exact (hA i hi).mono_left hV