Theorem: inter_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
⊢ Hpolytope ⋯ = Hpolytope hH_1 ∩ Hpolytope hH_2
Tactic:
ext x
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ Hpolytope hH_1 ∩ Hpolytope hH_2

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ Hpolytope hH_1 ∩ Hpolytope hH_2
Tactic:
rw [mem_Hpolytope, Set.mem_inter_iff, mem_Hpolytope, mem_Hpolytope]
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) ↔ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) ↔ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
constructor
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) → (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ ((∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α) → ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ (∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α) → (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
intro h
State after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
⊢ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α

State before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
⊢ (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
constructor <;> intro Hi_ hH_ <;> exact h Hi_ (by simp only [Set.mem_union, hH_, true_or, or_true])
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
Hi_ : Halfspace E
hH_ : Hi_ ∈ H_2
⊢ Hi_ ∈ H_1 ∪ H_2
Tactic:
simp only [Set.mem_union, hH_, true_or, or_true]
State after:
no goals

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
⊢ ((∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α) → ∀ Hi ∈ H_1 ∪ H_2, ↑Hi.f x ≤ Hi.α
Tactic:
intro h Hi hHi
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∪ H_2
⊢ ↑Hi.f x ≤ Hi.α

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∪ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rw [Set.mem_union] at hHi
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∨ Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1 ∨ Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rcases hHi with hHi | hHi
State after:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1
⊢ ↑Hi.f x ≤ Hi.α

case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α

State before:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_1
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h.1 Hi hHi
State after:
no goals

State before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
hH_1 : Set.Finite H_1
hH_2 : Set.Finite H_2
x : E
h : (∀ Hi ∈ H_1, ↑Hi.f x ≤ Hi.α) ∧ ∀ Hi ∈ H_2, ↑Hi.f x ≤ Hi.α
Hi : Halfspace E
hHi : Hi ∈ H_2
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
exact h.2 Hi hHi
State after:
no goals