𝕜 : Type u_1
𝕜₂ : Type ?u.427366
𝕝 : Type ?u.427369
𝕝₂ : Type ?u.427372
E : Type u_2
F : Type u_4
G : Type ?u.427381
ι : Type u_3
ι' : Type ?u.427387
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in Filter.atTop, ↑(p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → ↑(p i) (u x - y₀) < ε
𝕜 : Type u_1
𝕜₂ : Type ?u.427366
𝕝 : Type ?u.427369
𝕝₂ : Type ?u.427372
E : Type u_2
F : Type u_4
G : Type ?u.427381
ι : Type u_3
ι' : Type ?u.427387
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ Filter.Tendsto u Filter.atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → ↑(p i) (u x - y₀) < ε
rw [hp.tendsto_nhds u y₀]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.427366
𝕝 : Type ?u.427369
𝕝₂ : Type ?u.427372
E : Type u_2
F : Type u_4
G : Type ?u.427381
ι : Type u_3
ι' : Type ?u.427387
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in Filter.atTop, ↑(p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → ↑(p i) (u x - y₀) < ε
exact forall₃_congr fun _ _ _ => Filter.eventually_atTop