Theorem: Halfspace_translation.S (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
⊢ ↑(Halfspace_translation x H_) = (fun x_1 => x_1 + x) '' ↑H_
Tactic:
ext y
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y ∈ (fun x_1 => x_1 + x) '' ↑H_

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y ∈ (fun x_1 => x_1 + x) '' ↑H_
Tactic:
rw [Halfspace_translation, Halfspace_mem, Set.image_add_right, Set.mem_preimage, ← sub_eq_add_neg,
  Halfspace_mem, ContinuousLinearMap.map_sub, sub_le_iff_le_add]
State after:
no goals