case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
⊢ Pointed K
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
ne : Set.Nonempty ↑K
hc : IsClosed ↑K
⊢ Pointed K
obtain ⟨x, hx⟩ := ne
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ Pointed K
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ Pointed K
have fI : f '' Set.Ioi 0 ⊆ (K : Set H) := by
  rintro _ ⟨_, h, rfl⟩
  exact K.smul_mem (Set.mem_Ioi.1 h) hx
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ Pointed K
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
⊢ Pointed K
have clf : closure (f '' Set.Ioi 0) ⊆ (K : Set H) := hc.closure_subset_iff.2 fI
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ Pointed K
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
⊢ Pointed K
have fc : ContinuousWithinAt f (Set.Ioi (0 : ℝ)) 0 :=
  (continuous_id.smul continuous_const).continuousWithinAt
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ Pointed K
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ Pointed K
have mem₀ := fc.mem_closure_image (by rw [closure_Ioi (0 : ℝ), mem_Ici])
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ Pointed K
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
⊢ Pointed K
have f₀ : f 0 = 0 := zero_smul ℝ x
no goals
case intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
mem₀ : f 0 ∈ closure (f '' Ioi 0)
f₀ : f 0 = 0
⊢ Pointed K
simpa only [f₀, ConvexCone.Pointed, ← SetLike.mem_coe] using mem_of_subset_of_mem clf mem₀
case intro.intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
⊢ f '' Ioi 0 ⊆ ↑K
rintro _ ⟨_, h, rfl⟩
no goals
case intro.intro
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
w✝ : ℝ
h : w✝ ∈ Ioi 0
⊢ f w✝ ∈ ↑K
exact K.smul_mem (Set.mem_Ioi.1 h) hx
no goals
𝕜 : Type ?u.96025
E : Type ?u.96028
F : Type ?u.96031
G : Type ?u.96034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
K : ConvexCone ℝ H
hc : IsClosed ↑K
x : H
hx : x ∈ ↑K
f : ℝ → H := fun x_1 => x_1 • x
fI : f '' Ioi 0 ⊆ ↑K
clf : closure (f '' Ioi 0) ⊆ ↑K
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)
rw [closure_Ioi (0 : ℝ), mem_Ici]