Theorem: inter_cutSpace (src/Cutspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
⊢ cutSpace (H_1 ∪ H_2) = cutSpace H_1 ∩ cutSpace H_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)
x : E
⊢ x ∈ cutSpace (H_1 ∪ H_2) ↔ x ∈ cutSpace H_1 ∩ cutSpace H_2

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
x : E
⊢ x ∈ cutSpace (H_1 ∪ H_2) ↔ x ∈ cutSpace H_1 ∩ cutSpace H_2
Tactic:
rw [mem_cutSpace, Set.mem_inter_iff, mem_cutSpace, mem_cutSpace]
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_1 H_2 : Set (Halfspace E)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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