case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ UniqueDiffWithinAt ℝ s x
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
hs : Set.Nonempty (interior s)
x : G
hx : x ∈ closure s
⊢ UniqueDiffWithinAt ℝ s x
rcases hs with ⟨y, hy⟩
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ UniqueDiffWithinAt ℝ s x
suffices y - x ∈ interior (tangentConeAt ℝ s x) by
  refine' ⟨Dense.of_closure _, hx⟩
  simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
      ⟨y - x, interior_mono Submodule.subset_span this⟩]
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)
rw [mem_interior_iff_mem_nhds]
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ (fun x_1 => x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)
apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
case intro.intro.intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ (fun x_1 => x_1 - x) z ∈ tangentConeAt ℝ s x
case intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ (fun x_1 => x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x
rintro _ ⟨z, zs, rfl⟩
case intro.intro.intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s
case intro.intro.intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ (fun x_1 => x_1 - x) z ∈ tangentConeAt ℝ s x
refine' mem_tangentCone_of_openSegment_subset (Subset.trans _ interior_subset)
no goals
case intro.intro.intro
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s
exact conv.openSegment_closure_interior_subset_interior hx zs
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Dense (closure ↑(Submodule.span ℝ (tangentConeAt ℝ s x)))
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ UniqueDiffWithinAt ℝ s x
refine' ⟨Dense.of_closure _, hx⟩
no goals
𝕜 : Type ?u.165851
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.165857
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.165952
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x✝ y✝ : E
s✝ t : Set E
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Dense (closure ↑(Submodule.span ℝ (tangentConeAt ℝ s x)))
simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    ⟨y - x, interior_mono Submodule.subset_span this⟩]