R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ↑f
h : Wbtw R (↑f x) (↑f y) (↑f z)
⊢ Wbtw R x y z
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ↑f
⊢ Wbtw R (↑f x) (↑f y) (↑f z) ↔ Wbtw R x y z
refine' ⟨fun h => _, fun h => h.map _⟩
no goals
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ↑f
h : Wbtw R (↑f x) (↑f y) (↑f z)
⊢ Wbtw R x y z
rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h