R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ ↑(lineMap y (↑(pointReflection R x) y)) 2⁻¹ = x
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R y x (↑(pointReflection R x) y)
refine' ⟨2⁻¹, ⟨by norm_num, by norm_num⟩, _⟩
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ • 2 • (x -ᵥ y) +ᵥ y = x
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ ↑(lineMap y (↑(pointReflection R x) y)) 2⁻¹ = x
rw [lineMap_apply, pointReflection_apply, vadd_vsub_assoc, ← two_smul R (x -ᵥ y)]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ • 2 • (x -ᵥ y) +ᵥ y = x
simp
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 0 ≤ 2⁻¹
norm_num
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.618495
P : Type u_3
P' : Type ?u.618501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ ≤ 1
norm_num