internlm/Lean-Github huggingface dataset:
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
rw [SetLike.ext_iff] at h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : ∀ (x_1 : E), x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H1 ↔ x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : ∀ (x_1 : E), x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H1 ↔ x_1 ∈ (fun x_2 => Halfspace_translation x x_2) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
specialize h (y + x)
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y + x ∈ (fun x_1 => Halfspace_translation x x_1) H1 ↔ y + x ∈ (fun x_1 => Halfspace_translation x x_1) H2
⊢ y ∈ H1 ↔ y ∈ H2
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y + x ∈ (fun x_1 => Halfspace_translation x x_1) H1 ↔ y + x ∈ (fun x_1 => Halfspace_translation x x_1) H2
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
rw [← SetLike.mem_coe, ← SetLike.mem_coe, mem_Halfspace_translation, mem_Halfspace_translation, add_sub_cancel] at h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y ∈ ↑H1 ↔ y ∈ ↑H2
⊢ y ∈ H1 ↔ y ∈ H2
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
y : E
h : y ∈ ↑H1 ↔ y ∈ ↑H2
⊢ y ∈ H1 ↔ y ∈ H2
Tactic:
exact h
Proof state after:
no goals
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
have := ContinuousLinearMap.frontier_preimage Hi_.f.1 (unitSphereDual_surj Hi_.f) (Set.Iic Hi_.α)
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' frontier (Set.Iic Hi_.α)
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' frontier (Set.Iic Hi_.α)
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
simp only [ne_eq, LinearMap.coe_toContinuousLinearMap', Set.nonempty_Ioi, frontier_Iic'] at this
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' Set.Iic Hi_.α) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
change frontier ( Hi_.f.1 ⁻¹' {x | x ≤ Hi_.α}) = Hi_.f.1 ⁻¹' {Hi_.α} at this
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ frontier ↑Hi_ = {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Hi_.h, this]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
this : frontier (⇑↑Hi_.f ⁻¹' {x | x ≤ Hi_.α}) = ⇑↑Hi_.f ⁻¹' {Hi_.α}
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
clear this
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ ⇑↑Hi_.f ⁻¹' {Hi_.α} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
unfold Set.preimage
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ {x | ↑Hi_.f x ∈ {Hi_.α}} = {x | ↑Hi_.f x = Hi_.α}
Theorem: frontierHalfspace_Hyperplane
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ {x | ↑Hi_.f x ∈ {Hi_.α}} = {x | ↑Hi_.f x = Hi_.α}
Tactic:
simp only [ne_eq, Set.mem_singleton_iff]
Proof state after:
no goals
Theorem: Hyperplane_convex
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ Convex ℝ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact @convex_hyperplane ℝ E ℝ _ _ _ _ _ _ Hi_.f.1 (LinearMap.isLinear Hi_.f.1) Hi_.α
Proof state after:
no goals
Theorem: Hyperplane_affineClosed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
⊢ ∀ (s : Fin n → E),
    Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α} →
      ∀ (a : Fin n → ℝ),
        Finset.sum Finset.univ a = 1 → (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
intro s hs a ha
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}
Theorem: Hyperplane_affineClosed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.affineCombination ℝ Finset.univ s) a ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Finset.affineCombination_eq_linear_combination _ _ _ ha, Set.mem_setOf, map_sum]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Tactic:
have hg : (fun i => Hi_.f.1 (a i • s i)) = fun i => a i * Hi_.α := by
  ext i
  rw [Set.range_subset_iff] at hs
  specialize hs i
  rw [Set.mem_setOf] at hs
  rw [ContinuousLinearMap.map_smulₛₗ, smul_eq_mul, RingHom.id_apply, hs]
  done
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
hg : (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
hg : (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
⊢ (Finset.sum Finset.univ fun x => ↑Hi_.f (a x • s x)) = Hi_.α
Tactic:
rw [hg, ←Finset.sum_mul, ha, one_mul]
Proof state after:
no goals
Theorem: Hyperplane_affineClosed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
⊢ (fun i => ↑Hi_.f (a i • s i)) = fun i => a i * Hi_.α
Tactic:
ext i
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : Set.range s ⊆ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [Set.range_subset_iff] at hs
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : ∀ (y : Fin n), s y ∈ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
hs : ∀ (y : Fin n), s y ∈ {x | ↑Hi_.f x = Hi_.α}
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
specialize hs i
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : s i ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : s i ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [Set.mem_setOf] at hs
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : ↑Hi_.f (s i) = Hi_.α
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Theorem: Hyperplane_affineClosed
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
Hi_ : Halfspace E
s : Fin n → E
a : Fin n → ℝ
ha : Finset.sum Finset.univ a = 1
i : Fin n
hs : ↑Hi_.f (s i) = Hi_.α
⊢ ↑Hi_.f (a i • s i) = a i * Hi_.α
Tactic:
rw [ContinuousLinearMap.map_smulₛₗ, smul_eq_mul, RingHom.id_apply, hs]
Proof state after:
no goals
Theorem: Halfspace.val_raw
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∃ H_, ((∀ (x : ↥p), ↑H_.f ↑x = ↑H_'.f x) ∧ ‖↑H_.f‖ = ‖↑H_'.f‖) ∧ H_.α = H_'.α
Tactic:
rcases H_' with ⟨ ⟨ f, hf ⟩, C ⟩
Proof state after:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Theorem: Halfspace.val_raw
Proof state before:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Tactic:
choose g hg using Real.exists_extension_norm_eq p f
Proof state after:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
g : E →L[ℝ] ℝ
hg : (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Theorem: Halfspace.val_raw
Proof state before:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
g : E →L[ℝ] ℝ
hg : (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Tactic:
exact ⟨ ⟨ ⟨ g, hg.2 ▸ hf ⟩, C ⟩, hg, rfl ⟩
Proof state after:
no goals
Theorem: Halfspace.val_f
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
Tactic:
unfold val
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∀ (x : ↥p), ↑((fun H_ x => H_) (Classical.choose ⋯) ⋯).f ↑x = ↑H_'.f x
Theorem: Halfspace.val_f
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∀ (x : ↥p), ↑((fun H_ x => H_) (Classical.choose ⋯) ⋯).f ↑x = ↑H_'.f x
Tactic:
exact (Classical.choose_spec (Halfspace.val_raw p H_')).1.1
Proof state after:
no goals
Theorem: Halfspace.val_C
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ (val p H_').α = H_'.α
Tactic:
unfold val
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ((fun H_ x => H_) (Classical.choose ⋯) ⋯).α = H_'.α
Theorem: Halfspace.val_C
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ((fun H_ x => H_) (Classical.choose ⋯) ⋯).α = H_'.α
Tactic:
exact (Classical.choose_spec (Halfspace.val_raw p H_')).2
Proof state after:
no goals
Theorem: Halfspace.val_eq
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'
Tactic:
have := Halfspace.val_f p H_'
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'
Theorem: Halfspace.val_eq
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'
Tactic:
apply subset_antisymm <;> intro x <;> rw [Set.mem_inter_iff, Set.mem_image]
Proof state after:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x

case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p
Theorem: Halfspace.val_eq
Proof state before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
rintro ⟨ hxH_', hxp ⟩
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x
Theorem: Halfspace.val_eq
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
refine ⟨ ⟨ x, hxp ⟩, ?_, rfl ⟩
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'
Theorem: Halfspace.val_eq
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'
Tactic:
rw [Halfspace_mem, ← (this ⟨ x, hxp ⟩), ← Halfspace.val_C p H_']
Proof state after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α
Theorem: Halfspace.val_eq
Proof state before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α
Tactic:
exact hxH_'
Proof state after:
no goals
Theorem: Halfspace.val_eq
Proof state before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p
Tactic:
rintro ⟨ ⟨ x', hx'p ⟩, hx'H_', rfl ⟩
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p
Theorem: Halfspace.val_eq
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p
Tactic:
refine ⟨ ?_, hx'p ⟩
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Theorem: Halfspace.val_eq
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
rw [Halfspace_mem, ← (this ⟨ x', hx'p ⟩), ← Halfspace.val_C p H_'] at hx'H_'
Proof state after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Theorem: Halfspace.val_eq
Proof state before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
exact hx'H_'
Proof state after:
no goals
Theorem: Halfspace.val_eq'
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
⊢ ∀ (H_' : Halfspace ↥p), (fun H_ => ↑(val p H_) ∩ ↑p) H_' = (fun H_ => Subtype.val '' H_) ↑H_'
Tactic:
intro H_'
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ (fun H_ => ↑(val p H_) ∩ ↑p) H_' = (fun H_ => Subtype.val '' H_) ↑H_'
Theorem: Halfspace.val_eq'
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ (fun H_ => ↑(val p H_) ∩ ↑p) H_' = (fun H_ => Subtype.val '' H_) ↑H_'
Tactic:
have := Halfspace.val_f p H_'
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ (fun H_ => ↑(val p H_) ∩ ↑p) H_' = (fun H_ => Subtype.val '' H_) ↑H_'