internlm/Lean-Github huggingface dataset:
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ∀ x ∈ a.support, (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) x (a x) = 0
Tactic:
intro i _
Proof state after:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
i : ι
a✝ : i ∈ a.support
⊢ (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) i (a i) = 0
Theorem: Submodule.mem_orthogonal_Basis
Proof state before:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
i : ι
a✝ : i ∈ a.support
⊢ (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) i (a i) = 0
Tactic:
simp only [h i, smul_eq_mul, mul_zero]
Proof state after:
no goals
Theorem: AffineMap.preimage_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
have h1 := Set.image_preimage_eq_of_subset hs
Proof state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)
Theorem: AffineMap.preimage_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
⊢ ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
ext x
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
x : E
⊢ x ∈ ⇑f ⁻¹' (convexHull 𝕜) s ↔ x ∈ (convexHull 𝕜) (⇑f ⁻¹' s)
Theorem: AffineMap.preimage_convexHull
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
f : E →ᵃ[𝕜] F
hf : Function.Injective f.toFun
hs : s ⊆ Set.range ⇑f
h1 : ⇑f '' (⇑f ⁻¹' s) = s
x : E
⊢ x ∈ ⇑f ⁻¹' (convexHull 𝕜) s ↔ x ∈ (convexHull 𝕜) (⇑f ⁻¹' s)
Tactic:
rw [Set.mem_preimage, ← Function.Injective.mem_set_image hf, AffineMap.toFun_eq_coe, AffineMap.image_convexHull, h1]
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
i : Fin n
⊢ i ∈ Nat.fin_list_range n
Tactic:
induction n with
| zero => exact i.elim0
| succ n ih =>
  match i with
  | 0 => exact List.mem_cons_self _ _
  | (mk (Nat.succ m) h) =>
    have : m < n := by omega
    let m' : Fin n := ⟨m, this⟩
    unfold Nat.fin_list_range
    apply List.mem_cons_of_mem
    simp only [List.mem_map]
    use m'
    use ih m'
    rfl
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
case zero
i : Fin Nat.zero
⊢ i ∈ Nat.fin_list_range Nat.zero
Tactic:
exact i.elim0
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
case succ
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
⊢ i ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
match i with
| 0 => exact List.mem_cons_self _ _
| (mk (Nat.succ m) h) =>
  have : m < n := by omega
  let m' : Fin n := ⟨m, this⟩
  unfold Nat.fin_list_range
  apply List.mem_cons_of_mem
  simp only [List.mem_map]
  use m'
  use ih m'
  rfl
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
⊢ 0 ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
exact List.mem_cons_self _ _
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
have : m < n := by omega
Proof state after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
let m' : Fin n := ⟨m, this⟩
Proof state after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ Nat.fin_list_range (Nat.succ n)
Tactic:
unfold Nat.fin_list_range
Proof state after:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ 0 :: List.map succ (Nat.fin_list_range n)
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ 0 :: List.map succ (Nat.fin_list_range n)
Tactic:
apply List.mem_cons_of_mem
Proof state after:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ List.map succ (Nat.fin_list_range n)
Theorem: Fin.mem_fin_list_range
Proof state before:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ { val := Nat.succ m, isLt := h } ∈ List.map succ (Nat.fin_list_range n)
Tactic:
simp only [List.mem_map]
Proof state after:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ ∃ a ∈ Nat.fin_list_range n, succ a = { val := Nat.succ m, isLt := h }
Theorem: Fin.mem_fin_list_range
Proof state before:
case a
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ ∃ a ∈ Nat.fin_list_range n, succ a = { val := Nat.succ m, isLt := h }
Tactic:
use m'
Proof state after:
case h
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ m' ∈ Nat.fin_list_range n ∧ succ m' = { val := Nat.succ m, isLt := h }
Theorem: Fin.mem_fin_list_range
Proof state before:
case h
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ m' ∈ Nat.fin_list_range n ∧ succ m' = { val := Nat.succ m, isLt := h }
Tactic:
use ih m'
Proof state after:
case right
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ succ m' = { val := Nat.succ m, isLt := h }
Theorem: Fin.mem_fin_list_range
Proof state before:
case right
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
this : m < n
m' : Fin n := { val := m, isLt := this }
⊢ succ m' = { val := Nat.succ m, isLt := h }
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.mem_fin_list_range
Proof state before:
n : ℕ
ih : ∀ (i : Fin n), i ∈ Nat.fin_list_range n
i : Fin (Nat.succ n)
m : ℕ
h : Nat.succ m < Nat.succ n
⊢ m < n
Tactic:
omega
Proof state after:
no goals
Theorem: pointDual.α
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ (pointDual p).α = ‖↑p‖⁻¹
Tactic:
rfl
Proof state after:
no goals
Theorem: pointDual.h
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ ↑(pointDual p) = ⇑((InnerProductSpace.toDual ℝ E) (‖↑p‖⁻¹ • ↑p)) ⁻¹' {x | x ≤ ‖↑p‖⁻¹}
Tactic:
rfl
Proof state after:
no goals
Theorem: pointDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ∈ ↑(pointDual p)
Tactic:
rw [pointDual.h, map_smulₛₗ, map_inv₀, IsROrC.conj_to_real, Set.preimage_setOf_eq,
  Set.mem_setOf_eq, map_zero, ← one_div]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ≤ 1 / ‖↑p‖
Theorem: pointDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ≤ 1 / ‖↑p‖
Tactic:
apply le_of_lt
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 / ‖↑p‖
Theorem: pointDual_origin
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 / ‖↑p‖
Tactic:
rw [div_pos_iff]
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖ ∨ 1 < 0 ∧ ‖↑p‖ < 0
Theorem: pointDual_origin
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖ ∨ 1 < 0 ∧ ‖↑p‖ < 0
Tactic:
left
Proof state after:
case a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖
Theorem: pointDual_origin
Proof state before:
case a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖
Tactic:
exact ⟨ zero_lt_one, by rw [norm_pos_iff]; exact p.2 ⟩
Proof state after:
no goals
Theorem: pointDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < ‖↑p‖
Tactic:
rw [norm_pos_iff]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ ↑p ≠ 0
Theorem: pointDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ ↑p ≠ 0
Tactic:
exact p.2
Proof state after:
no goals
Theorem: mem_pointDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ x ∈ ↑(pointDual p) ↔ ⟪↑p, x⟫_ℝ ≤ 1
Tactic:
rw [pointDual.h, Set.mem_preimage, InnerProductSpace.toDual_apply, Set.mem_setOf,
  inner_smul_left, IsROrC.conj_to_real, ← mul_le_mul_left (by rw [norm_pos_iff]; exact p.2 : 0 < norm p.1),
  ← mul_assoc, mul_inv_cancel (norm_ne_zero_iff.mpr p.2), one_mul]
Proof state after:
no goals
Theorem: mem_pointDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ 0 < ‖↑p‖
Tactic:
rw [norm_pos_iff]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ ↑p ≠ 0
Theorem: mem_pointDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ ↑p ≠ 0
Tactic:
exact p.2
Proof state after:
no goals
Theorem: pointDual_comm
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p q : { p // p ≠ 0 }
⊢ ↑p ∈ ↑(pointDual q) ↔ ↑q ∈ ↑(pointDual p)
Tactic:
rw [mem_pointDual, mem_pointDual, real_inner_comm]
Proof state after:
no goals
Theorem: polarDual_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ IsClosed (polarDual X)
Tactic:
apply isClosed_sInter
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), IsClosed t
Theorem: polarDual_closed
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), IsClosed t
Tactic:
intro Hi_s h
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ IsClosed Hi_s
Theorem: polarDual_closed
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ IsClosed Hi_s
Tactic:
rw [Set.mem_image] at h
Proof state after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ IsClosed Hi_s
Theorem: polarDual_closed
Proof state before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ IsClosed Hi_s
Tactic:
rcases h with ⟨ Hi_, _, rfl ⟩
Proof state after:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ IsClosed ↑Hi_
Theorem: polarDual_closed
Proof state before:
case a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ IsClosed ↑Hi_
Tactic:
exact Halfspace_closed _
Proof state after:
no goals
Theorem: polarDual_convex
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ Convex ℝ (polarDual X)
Tactic:
apply convex_sInter
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), Convex ℝ s
Theorem: polarDual_convex
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ ∀ s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), Convex ℝ s
Tactic:
intro Hi_s h
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ Convex ℝ Hi_s
Theorem: polarDual_convex
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ Convex ℝ Hi_s
Tactic:
rw [Set.mem_image] at h
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ Convex ℝ Hi_s
Theorem: polarDual_convex
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ Convex ℝ Hi_s
Tactic:
rcases h with ⟨ Hi_, _, rfl ⟩
Proof state after:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ Convex ℝ ↑Hi_
Theorem: polarDual_convex
Proof state before:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
left✝ : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex _
Proof state after:
no goals
Theorem: polarDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ 0 ∈ polarDual X
Tactic:
intro Hi_s h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ 0 ∈ Hi_s
Theorem: polarDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ 0 ∈ Hi_s
Tactic:
rw [Set.mem_image] at h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ 0 ∈ Hi_s
Theorem: polarDual_origin
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ 0 ∈ Hi_s
Tactic:
rcases h with ⟨ Hi_, h, rfl ⟩
Proof state after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ 0 ∈ ↑Hi_
Theorem: polarDual_origin
Proof state before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ 0 ∈ ↑Hi_
Tactic:
rw [Set.mem_image] at h
Proof state after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ 0 ∈ ↑Hi_
Theorem: polarDual_origin
Proof state before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ 0 ∈ ↑Hi_
Tactic:
rcases h with ⟨ p, _, rfl ⟩
Proof state after:
case intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
p : { p // p ≠ 0 }
left✝ : p ∈ Subtype.val ⁻¹' X
⊢ 0 ∈ ↑(pointDual p)
Theorem: polarDual_origin
Proof state before:
case intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
p : { p // p ≠ 0 }
left✝ : p ∈ Subtype.val ⁻¹' X
⊢ 0 ∈ ↑(pointDual p)
Tactic:
exact pointDual_origin p
Proof state after:
no goals
Theorem: mem_polarDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ polarDual X ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
unfold polarDual
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [Set.mem_sInter]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) ↔ ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
constructor
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) → ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1) → ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
Theorem: mem_polarDual
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ (∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t) → ∀ x ∈ X, ⟪x, v⟫_ℝ ≤ 1
Tactic:
intro h x hx
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
⊢ ⟪x, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
cases' (em (x = 0)) with hx0 hx0
Proof state after:
case mp.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1

case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
specialize h (SetLike.coe <| pointDual ⟨ x, hx0 ⟩) ?_
Proof state after:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
h : ∀ t ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X)), v ∈ t
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ↑(pointDual { val := x, property := hx0 }) ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))

case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : v ∈ ↑(pointDual { val := x, property := hx0 })
⊢ ⟪x, v⟫_ℝ ≤ 1
Theorem: mem_polarDual
Proof state before:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : v ∈ ↑(pointDual { val := x, property := hx0 })
⊢ ⟪x, v⟫_ℝ ≤ 1
Tactic:
rw [mem_pointDual] at h
Proof state after:
case mp.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v x : E
hx : x ∈ X
hx0 : ¬x = 0
h : ⟪↑{ val := x, property := hx0 }, v⟫_ℝ ≤ 1
⊢ ⟪x, v⟫_ℝ ≤ 1