internlm/Lean-Github huggingface dataset:
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof 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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rcases Hpolytope_of_Vpolytope_interior _ hVinterior with ⟨ H_', hH_', hHV ⟩
Proof state after:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof state before:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
have hH_inter := inter_Hpolytope H_' H_ hH_' hH_
Proof state after:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof state before:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
have : IsCompact (Vpolytope hS ∩ Hpolytope hH_) := (Compact_Vpolytope hS).inter_right (Closed_cutSpace H_)
Proof state after:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Vpolytope hS ∩ Hpolytope hH_)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof state before:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Vpolytope hS ∩ Hpolytope hH_)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rw [← hHV, ← hH_inter] at this
Proof state after:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof state before:
case intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rcases Vpolytope_of_Hpolytope (hH_'.union hH_) this with ⟨ S', hS', hSV ⟩
Proof state after:
case intro.intro.intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof state before:
case intro.intro.intro.intro
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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ ∃ S', ∃ (hS' : Set.Finite S'), Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
exact ⟨ S', hS', by rw [← hSV, ← hHV, ← hH_inter] ⟩
Proof state after:
no goals
Theorem: Vpolytope_of_Vpolytope_inter_cutSpace_fin
Proof 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
hS : Set.Finite S
hVinterior : Set.Nonempty (interior (Vpolytope hS))
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
H_' : Set (Halfspace E)
hH_' : Set.Finite H_'
hHV : Hpolytope hH_' = Vpolytope hS
hH_inter : Hpolytope ⋯ = Hpolytope hH_' ∩ Hpolytope hH_
this : IsCompact (Hpolytope ⋯)
S' : Set E
hS' : Set.Finite S'
hSV : Hpolytope ⋯ = Vpolytope hS'
⊢ Vpolytope hS' = Vpolytope hS ∩ Hpolytope hH_
Tactic:
rw [← hSV, ← hHV, ← hH_inter]
Proof state after:
no goals
Theorem: InDown_eq_DownIn
Proof 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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
⊢ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) = Subtype.val ⁻¹' (S -ᵥ {↑x})
Tactic:
ext y
Proof state after:
case h
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ y ∈ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) ↔ y ∈ Subtype.val ⁻¹' (S -ᵥ {↑x})
Theorem: InDown_eq_DownIn
Proof state before:
case h
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ y ∈ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) ↔ y ∈ Subtype.val ⁻¹' (S -ᵥ {↑x})
Tactic:
simp only [AffineIsometryEquiv.coe_VSubconst, Set.vsub_singleton, Set.mem_image, Set.mem_preimage,
  Set.mem_image, Subtype.exists, exists_and_left]
Proof state after:
case h
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) ↔ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y
Theorem: InDown_eq_DownIn
Proof state before:
case h
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) ↔ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y
Tactic:
constructor
Proof state after:
case h.mp
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) → ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y

case h.mpr
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y) → ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Theorem: InDown_eq_DownIn
Proof state before:
case h.mp
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) → ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y
Tactic:
rintro ⟨ v, hvmemS, ⟨ hvmemp, rfl ⟩ ⟩
Proof state after:
case h.mp.intro.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Theorem: InDown_eq_DownIn
Proof state before:
case h.mp.intro.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Tactic:
refine ⟨ v, hvmemS, ?_ ⟩
Proof state after:
case h.mp.intro.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ v -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Theorem: InDown_eq_DownIn
Proof state before:
case h.mp.intro.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ v -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Tactic:
simp only [hvmemS, AffineSubspace.coe_vsub]
Proof state after:
no goals
Theorem: InDown_eq_DownIn
Proof state before:
case h.mpr
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y) → ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
rintro ⟨ v, hvmemS, h ⟩
Proof state after:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Theorem: InDown_eq_DownIn
Proof state before:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
have := y.2
Proof state after:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : ↑y ∈ AffineSubspace.direction p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Theorem: InDown_eq_DownIn
Proof state before:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : ↑y ∈ AffineSubspace.direction p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
rw [← h, AffineSubspace.vsub_right_mem_direction_iff_mem x.2] at this
Proof state after:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : v ∈ p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Theorem: InDown_eq_DownIn
Proof state before:
case h.mpr.intro.intro
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
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : v ∈ p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
exact ⟨ v, hvmemS, this, Subtype.val_injective ((AffineSubspace.coe_vsub _ _ x) ▸ h) ⟩
Proof state after:
no goals
Theorem: Nonempty_iff_Nonempty_interior_in_direction
Proof 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
Proof 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
Theorem: Nonempty_iff_Nonempty_interior_in_direction
Proof 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
Proof state after:
no goals
Theorem: Nonempty_iff_Nonempty_interior_in_direction
Proof 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
Proof 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)))
Theorem: Nonempty_iff_Nonempty_interior_in_direction
Proof 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]
Proof 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))
Theorem: Nonempty_iff_Nonempty_interior_in_direction
Proof 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
Proof state after:
no goals