Theorem: Halfspace_mem (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ∀ (x : E), x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α
Tactic:
intro x
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α
Tactic:
rw [H_.h]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ⇑↑H_.f ⁻¹' {x | x ≤ H_.α} ↔ ↑H_.f x ≤ H_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ⇑↑H_.f ⁻¹' {x | x ≤ H_.α} ↔ ↑H_.f x ≤ H_.α
Tactic:
rfl
State after:
no goals