Theorem: mem_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
⊢ x ∈ Hpolytope hH_ ↔ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Tactic:
constructor <;> intro h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
⊢ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ Hpolytope hH_

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
⊢ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Tactic:
intro Hi HiH
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ Hpolytope hH_
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
unfold Hpolytope at h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ ⋂₀ (SetLike.coe '' H_)
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : x ∈ ⋂₀ (SetLike.coe '' H_)
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Set.mem_sInter] at h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ t ∈ SetLike.coe '' H_, x ∈ t
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ t ∈ SetLike.coe '' H_, x ∈ t
Hi : Halfspace E
HiH : Hi ∈ H_
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
specialize h Hi ⟨ Hi, HiH, rfl ⟩
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : x ∈ ↑Hi
⊢ ↑Hi.f x ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : x ∈ ↑Hi
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Halfspace_mem] at h
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : ↑Hi.f x ≤ Hi.α
⊢ ↑Hi.f x ≤ Hi.α

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi : Halfspace E
HiH : Hi ∈ H_
h : ↑Hi.f x ≤ Hi.α
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h
State after:
no goals

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ Hpolytope hH_
Tactic:
unfold Hpolytope
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ ⋂₀ (SetLike.coe '' H_)

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ x ∈ ⋂₀ (SetLike.coe '' H_)
Tactic:
rw [Set.mem_sInter]
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ ∀ t ∈ SetLike.coe '' H_, x ∈ t

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
⊢ ∀ t ∈ SetLike.coe '' H_, x ∈ t
Tactic:
rintro _ ⟨ Hi_, hHi_, rfl ⟩
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x ∈ ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
h : ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x ∈ ↑Hi_
Tactic:
specialize h Hi_ hHi_
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ x ∈ ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ x ∈ ↑Hi_
Tactic:
rw [Halfspace_mem]
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ ↑Hi_.f x ≤ Hi_.α

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
h : ↑Hi_.f x ≤ Hi_.α
⊢ ↑Hi_.f x ≤ Hi_.α
Tactic:
exact h
State after:
no goals