𝕜 : Type u_1
𝕜₂ : Type ?u.423602
𝕝 : Type ?u.423605
𝕝₂ : Type ?u.423608
E : Type u_2
F : Type u_4
G : Type ?u.423617
ι : Type u_3
ι' : Type ?u.423623
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(Finset.sup s p) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(p i) (u x - y₀) < ε
𝕜 : Type u_1
𝕜₂ : Type ?u.423602
𝕝 : Type ?u.423605
𝕝₂ : Type ?u.423608
E : Type u_2
F : Type u_4
G : Type ?u.423617
ι : Type u_3
ι' : Type ?u.423623
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(p i) (u x - y₀) < ε
rw [hp.tendsto_nhds' u y₀]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.423602
𝕝 : Type ?u.423605
𝕝₂ : Type ?u.423608
E : Type u_2
F : Type u_4
G : Type ?u.423617
ι : Type u_3
ι' : Type ?u.423623
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(Finset.sup s p) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(p i) (u x - y₀) < ε
exact
  ⟨fun h i => by simpa only [Finset.sup_singleton] using h {i}, fun h s ε hε =>
    (s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.423602
𝕝 : Type ?u.423605
𝕝₂ : Type ?u.423608
E : Type u_2
F : Type u_4
G : Type ?u.423617
ι : Type u_3
ι' : Type ?u.423623
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
h : ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(Finset.sup s p) (u x - y₀) < ε
i : ι
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(p i) (u x - y₀) < ε
simpa only [Finset.sup_singleton] using h {i}