Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset (LeanCamCombi/ConvexContinuous.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : IsOpen (Subtype.val ⁻¹' s)
hx : x ∈ s
⊢ ∃ t, x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
classical
lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
set x : affineSpan ℝ s := x with hx
clear_value x
subst hx
obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
  fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
    finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
    with hf
sorry
State after:
no goals

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : IsOpen (Subtype.val ⁻¹' s)
hx : x ∈ s
⊢ ∃ t, x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
State after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
set x : affineSpan ℝ s := x with hx
State after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ : ↥(affineSpan ℝ s)
x : ↥(affineSpan ℝ s) := x✝
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ : ↥(affineSpan ℝ s)
x : ↥(affineSpan ℝ s) := x✝
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
clear_value x
State after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ x : ↥(affineSpan ℝ s)
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ x : ↥(affineSpan ℝ s)
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
subst hx
State after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
State after:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
  fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
    finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
    with hf
State after:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
f : Finset (Fin (finrank ℝ ↥(vectorSpan ℝ s))) → ↥(vectorSpan ℝ s) :=
  fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
hf :
  f = fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s

State before:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
f : Finset (Fin (finrank ℝ ↥(vectorSpan ℝ s))) → ↥(vectorSpan ℝ s) :=
  fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
hf :
  f = fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
sorry
State after:
no goals