Theorem: Base.up (Ray/Misc/Continuation.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ᶠ (z : E) in 𝓝ˢ (closure s), p b.u z
Tactic:
apply Filter.eventually_of_mem (b.ot.mem_nhdsSet.mpr b.cover)
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ b.t, p b.u x

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ b.t, p b.u x
Tactic:
intro x m
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ p b.u x

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ p b.u x
Tactic:
refine b.congr (b.gp (b.y m) (b.yt m)) ?_
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ (𝓝 x).EventuallyEq (b.g (b.y m)) b.u

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ (𝓝 x).EventuallyEq (b.g (b.y m)) b.u
Tactic:
exact ((b.ug _).eventuallyEq_of_mem ((b.ot.inter isOpen_ball).mem_nhds ⟨m, b.yt m⟩)).symm
State after:
no goals