Theorem: Halfspace_span (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ affineSpan ℝ ↑H_ = ⊤
Tactic:
apply affineSpan_eq_top_of_nonempty_interior
State after:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (interior ((convexHull ℝ) ↑H_))

State before:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (interior ((convexHull ℝ) ↑H_))
Tactic:
apply Set.Nonempty.mono (?_ : H_.f.1 ⁻¹' (Metric.ball (H_.α -1) (1/2)) ⊆ (interior ((convexHull ℝ) H_.S)))
State after:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ interior ((convexHull ℝ) (Halfspace.S H_))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ interior ((convexHull ℝ) (Halfspace.S H_))
Tactic:
rw [IsOpen.subset_interior_iff (IsOpen.preimage (?_) Metric.isOpen_ball)]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ (convexHull ℝ) (Halfspace.S H_)

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ (convexHull ℝ) (Halfspace.S H_)

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
apply subset_trans ?_ (subset_convexHull ℝ (SetLike.coe H_))
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
intro x hx
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
rw [Set.mem_preimage, Real.ball_eq_Ioo, Set.mem_Ioo] at hx
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
rw [Halfspace_mem H_]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ ↑H_.f x ≤ H_.α

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ ↑H_.f x ≤ H_.α

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
linarith
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
exact H_.f.1.cont
State after:
no goals

State before:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))
Tactic:
cases' unitSphereDual_surj H_.f (H_.α -1) with x hx
State after:
case hs.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))

State before:
case hs.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))
Tactic:
use x
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
Tactic:
rw [Set.mem_preimage, Metric.mem_ball, dist_sub_eq_dist_add_right, hx, sub_add_cancel, dist_self]
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ 0 < 1 / 2

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ 0 < 1 / 2
Tactic:
linarith
State after:
no goals