Theorem: Nonempty_iff_Nonempty_interior_in_direction (src/MainTheorem.lean)

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS : Nonempty ↑S
⊢ s ∈ affineSpan ℝ S
Tactic:
apply subset_affineSpan
State after:
case a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS : Nonempty ↑S
⊢ s ∈ S

State before:
case a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS : Nonempty ↑S
⊢ s ∈ S
Tactic:
exact hs
State after:
no goals

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS : Nonempty ↑S
⊢ Set.Nonempty
    (interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S)))
Tactic:
rw [Set.nonempty_coe_sort, ← @convexHull_nonempty_iff ℝ, ← intrinsicInterior_nonempty (convex_convexHull ℝ S),
  intrinsicInterior, Set.image_nonempty, affineSpan_convexHull] at hS
State after:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS✝ : Nonempty ↑S
hS : Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Set.Nonempty
    (interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S)))

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS✝ : Nonempty ↑S
hS : Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Set.Nonempty
    (interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S)))
Tactic:
rw [← AffineIsometryEquiv.coe_toHomeomorph, ← Homeomorph.image_interior, Set.image_nonempty]
State after:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS✝ : Nonempty ↑S
hS : Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : InnerProductSpace ℝ E✝
inst✝⁶ : CompleteSpace E✝
E P : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : FiniteDimensional ℝ E
S : Set E
s : E
hs : s ∈ S
hS✝ : Nonempty ↑S
hS : Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ Set.Nonempty (interior (Subtype.val ⁻¹' (convexHull ℝ) S))
Tactic:
exact hS
State after:
no goals