[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicInterior 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicInterior]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicFrontier 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicFrontier]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicClosure 𝕜 ∅ = ∅
[PROOFSTEP]
simp [intrinsicClosure]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ Set.Nonempty (intrinsicClosure 𝕜 s) → Set.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
⊢ intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
[PROOFSTEP]
rintro h rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
t : Set P
x : P
h : intrinsicClosure 𝕜 ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact h intrinsicClosure_empty
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicInterior 𝕜 {x} = {x}
[PROOFSTEP]
simpa only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ, Subtype.range_coe] using
  coe_affineSpan_singleton _ _ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicFrontier 𝕜 {x} = ∅
[PROOFSTEP]
rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ x : P
⊢ intrinsicClosure 𝕜 {x} = {x}
[PROOFSTEP]
simpa only [intrinsicClosure, preimage_coe_affineSpan_singleton, closure_univ, image_univ, Subtype.range_coe] using
  coe_affineSpan_singleton _ _ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
h : s ⊆ t
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
[PROOFSTEP]
refine' image_subset_iff.2 fun x hx => _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ x ∈ Subtype.val ⁻¹' intrinsicClosure 𝕜 t
[PROOFSTEP]
refine' ⟨Set.inclusion (affineSpan_mono _ h) x, _, rfl⟩
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ inclusion (_ : affineSpan 𝕜 s ≤ affineSpan 𝕜 t) x ∈ closure (Subtype.val ⁻¹' t)
[PROOFSTEP]
refine' (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono _ hx)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x✝ : P
h : s ⊆ t
x : { x // x ∈ affineSpan 𝕜 s }
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Subtype.val ⁻¹' s ⊆ inclusion (_ : affineSpan 𝕜 s ≤ affineSpan 𝕜 t) ⁻¹' (Subtype.val ⁻¹' t)
[PROOFSTEP]
exact fun y hy => h hy
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ (fun a => ↑a) '' (closure (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) = intrinsicInterior 𝕜 s
[PROOFSTEP]
rw [closure_diff_frontier, intrinsicInterior]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
[PROOFSTEP]
simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier, image_union]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
[PROOFSTEP]
rw [union_comm, intrinsicInterior_union_intrinsicFrontier]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s
[PROOFSTEP]
rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
x : P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ s ⊆ range Subtype.val
[PROOFSTEP]
exact (subset_affineSpan _ _).trans Subtype.range_coe.superset
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s
[PROOFSTEP]
refine' IsClosed.intrinsicClosure _
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t✝ : Set P
x : P
s : Set P
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
clear_value t
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t✝ : Set P
x : P
s : Set P
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
obtain rfl := ht.trans (affineSpan_intrinsicClosure _)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
[PROOFSTEP]
rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s✝ t : Set P
x : P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (closure (Subtype.val ⁻¹' s))
[PROOFSTEP]
exact isClosed_closure
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicInterior 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicInterior 𝕜 ∅
[PROOFSTEP]
simp only [intrinsicInterior_empty, image_empty]
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicInterior 𝕜 (↑φ '' s) = ↑φ '' intrinsicInterior 𝕜 s
[PROOFSTEP]
rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
  Function.comp.assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm, ← preimage_comp,
  Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp,
  φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicFrontier 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicFrontier 𝕜 ∅
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicFrontier 𝕜 (↑φ '' s) = ↑φ '' intrinsicFrontier 𝕜 s
[PROOFSTEP]
rw [intrinsicFrontier, intrinsicFrontier, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
  Function.comp.assoc, image_comp, image_comp, f.symm.image_frontier, f.image_symm, ← preimage_comp,
  Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp,
  φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
⊢ intrinsicClosure 𝕜 (↑φ '' ∅) = ↑φ '' intrinsicClosure 𝕜 ∅
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
[GOAL]
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : MetricSpace P
inst✝² : PseudoMetricSpace Q
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedAddTorsor W Q
φ : P →ᵃⁱ[𝕜] Q
s : Set P
hs : Set.Nonempty s
this✝ : Nonempty ↑s
f : { x // x ∈ affineSpan 𝕜 s } ≃ₜ { x // x ∈ map φ.toAffineMap (affineSpan 𝕜 s) } :=
  AffineIsometryEquiv.toHomeomorph (isometryEquivMap φ (affineSpan 𝕜 s))
this : ↑φ.toAffineMap ∘ Subtype.val ∘ ↑(Homeomorph.symm f) = Subtype.val
⊢ intrinsicClosure 𝕜 (↑φ '' s) = ↑φ '' intrinsicClosure 𝕜 s
[PROOFSTEP]
rw [intrinsicClosure, intrinsicClosure, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ← Function.comp.assoc,
  image_comp, image_comp, f.symm.image_closure, f.image_symm, ← preimage_comp, Function.comp.assoc, f.symm_comp_self,
  AffineIsometry.coe_toAffineMap, Function.comp.right_id, preimage_comp, φ.injective.preimage_image]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = closure s
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure s
[PROOFSTEP]
simp only [mem_closure_iff, mem_intrinsicClosure]
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → y ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)) ∧ ↑y = x) ↔
    ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
refine' ⟨_, fun h => ⟨⟨x, _⟩, _, Subtype.coe_mk _ _⟩⟩
[GOAL]
case h.refine'_1
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → y ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)) ∧ ↑y = x) →
    ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
rintro ⟨x, h, rfl⟩ t ht hx
[GOAL]
case h.refine'_1.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : { x // x ∈ affineSpan 𝕜 s }
h : ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → x ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
t : Set P
ht : IsOpen t
hx : ↑x ∈ t
⊢ Set.Nonempty (t ∩ s)
[PROOFSTEP]
obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx
[GOAL]
case h.refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : { x // x ∈ affineSpan 𝕜 s }
h : ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }), IsOpen o → x ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
t : Set P
ht : IsOpen t
hx : ↑x ∈ t
z : { x // x ∈ affineSpan 𝕜 s }
hz₁ : z ∈ Subtype.val ⁻¹' t
hz₂ : z ∈ Subtype.val ⁻¹' s
⊢ Set.Nonempty (t ∩ s)
[PROOFSTEP]
exact ⟨z, hz₁, hz₂⟩
[GOAL]
case h.refine'_2
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
⊢ ∀ (o : Set { x // x ∈ affineSpan 𝕜 s }),
    IsOpen o → { val := x, property := ?h.refine'_3 } ∈ o → Set.Nonempty (o ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨t, ht, rfl⟩ hx
[GOAL]
case h.refine'_2.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
t : Set P
ht : IsOpen t
hx : { val := x, property := ?h.refine'_3 } ∈ Subtype.val ⁻¹' t
⊢ Set.Nonempty (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
obtain ⟨y, hyt, hys⟩ := h _ ht hx
[GOAL]
case h.refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
t : Set P
ht : IsOpen t
hx : { val := x, property := ?h.refine'_3 } ∈ Subtype.val ⁻¹' t
y : P
hyt : y ∈ t
hys : y ∈ s
⊢ Set.Nonempty (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s)
[PROOFSTEP]
exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩
[GOAL]
case h.refine'_3
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
⊢ x ∈ ↑(affineSpan 𝕜 s)
[PROOFSTEP]
by_contra hc
[GOAL]
case h.refine'_3
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
hc : ¬x ∈ ↑(affineSpan 𝕜 s)
⊢ False
[PROOFSTEP]
obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc
[GOAL]
case h.refine'_3.intro.intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
hc : ¬x ∈ ↑(affineSpan 𝕜 s)
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s))ᶜ
hz₂ : z ∈ s
⊢ False
[PROOFSTEP]
exact hz₁ (subset_affineSpan 𝕜 s hz₂)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ Set.Nonempty (interior s) ↔ Set.Nonempty (interior (↑φ ⁻¹' s))
[PROOFSTEP]
rw [← φ.image_symm, ← φ.symm.image_interior, nonempty_image_iff]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : Set.Nonempty s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
haveI := hsne.coe_sort
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : Set.Nonempty s
this : Nonempty ↑s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
obtain ⟨p, hp⟩ := hsne
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
let p' : _root_.affineSpan ℝ s := ⟨p, subset_affineSpan _ _ hp⟩
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : { x // x ∈ _root_.affineSpan ℝ s } := { val := p, property := (_ : p ∈ ↑(_root_.affineSpan ℝ s)) }
⊢ Set.Nonempty (intrinsicInterior ℝ s)
[PROOFSTEP]
rw [intrinsicInterior, nonempty_image_iff, aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
  Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
  AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]
[GOAL]
case intro
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : { x // x ∈ _root_.affineSpan ℝ s } := { val := p, property := (_ : p ∈ ↑(_root_.affineSpan ℝ s)) }
⊢ Convex ℝ
    (↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) ⁻¹'
      (Subtype.val ⁻¹' s))
[PROOFSTEP]
exact
  hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ Set.Nonempty (intrinsicInterior ℝ s) → Set.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty]
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
[PROOFSTEP]
rintro h rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact h intrinsicInterior_empty
