ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>(AffineSubspace.map f s).WOppSide (f x) (f y) ↔ s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>(AffineSubspace.map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P ≃ᵃ[R] P'<GOAL>(AffineSubspace.map (↑f) s).WOppSide (f x) (f y) ↔ s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P ≃ᵃ[R] P'<GOAL>(AffineSubspace.map (↑f) s).SOppSide (f x) (f y) ↔ s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WSameSide x y<GOAL>(↑s).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>(↑s).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WOppSide x y<GOAL>(↑s).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>(↑s).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>x ∉ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>y ∉ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>x ∉ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>y ∉ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.WSameSide x y ↔ s.WSameSide y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.SSameSide x y ↔ s.SSameSide y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.WOppSide x y ↔ s.WOppSide y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.SOppSide x y ↔ s.SOppSide y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬⊥.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬⊥.SSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬⊥.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬⊥.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<GOAL>s.WSameSide x x ↔ (↑s).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<GOAL>s.SSameSide x x ↔ (↑s).Nonempty ∧ x ∉ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>hx : x ∈ s<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>hy : y ∈ s<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>hx : x ∈ s<GOAL>s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>hy : y ∈ s<GOAL>s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>p₁ p₂ : P<VAR>x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>p₁ p₂ : P<VAR>x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>s.WSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>h : x ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>s.WSameSide ((AffineMap.lineMap x y) t) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>h : x ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>s.WSameSide y ((AffineMap.lineMap x y) t)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>p₁ p₂ : P<VAR>x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>p₁ p₂ : P<VAR>x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>s.WOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>h : x ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>s.WOppSide ((AffineMap.lineMap x y) t) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>h : x ∈ s<VAR>t : R<VAR>ht : t ≤ 0<GOAL>s.WOppSide y ((AffineMap.lineMap x y) t)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hx : x ∈ s<GOAL>s.WSameSide y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hx : x ∈ s<GOAL>s.WSameSide z y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hz : z ∈ s<GOAL>s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hz : z ∈ s<GOAL>s.WSameSide y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hy : y ∈ s<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>StrictOrderedCommRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hy : y ∈ s<GOAL>s.WOppSide z x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<GOAL>s.WOppSide x x ↔ x ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<GOAL>¬s.SOppSide x x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WSameSide x y<VAR>hyz : s.WSameSide y z<VAR>hy : y ∉ s<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WSameSide x y<VAR>hyz : s.SSameSide y z<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WSameSide x y<VAR>hyz : s.WOppSide y z<VAR>hy : y ∉ s<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WSameSide x y<VAR>hyz : s.SOppSide y z<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SSameSide x y<VAR>hyz : s.WSameSide y z<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SSameSide x y<VAR>hyz : s.SSameSide y z<GOAL>s.SSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SSameSide x y<VAR>hyz : s.WOppSide y z<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SSameSide x y<VAR>hyz : s.SOppSide y z<GOAL>s.SOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WOppSide x y<VAR>hyz : s.WSameSide y z<VAR>hy : y ∉ s<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WOppSide x y<VAR>hyz : s.SSameSide y z<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WOppSide x y<VAR>hyz : s.WOppSide y z<VAR>hy : y ∉ s<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.WOppSide x y<VAR>hyz : s.SOppSide y z<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SOppSide x y<VAR>hyz : s.WSameSide y z<GOAL>s.WOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SOppSide x y<VAR>hyz : s.SSameSide y z<GOAL>s.SOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SOppSide x y<VAR>hyz : s.WOppSide y z<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hxy : s.SOppSide x y<VAR>hyz : s.SOppSide y z<GOAL>s.SSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WSameSide x y<GOAL>¬s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>¬s.WOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<GOAL>¬s.SOppSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WOppSide x y<GOAL>¬s.SSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>¬s.WSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>¬s.SSameSide x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>∃ p ∈ s, Sbtw R x p y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>h : Sbtw R x y z<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>s.SOppSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 < t<GOAL>s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 < t<GOAL>s.SSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<VAR>t : R<VAR>ht : 0 < t<GOAL>s.SSameSide ((AffineMap.lineMap x y) t) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<VAR>t : R<VAR>ht : 0 < t<GOAL>s.SSameSide y ((AffineMap.lineMap x y) t)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t < 0<GOAL>s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t < 0<GOAL>s.SOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<VAR>t : R<VAR>ht : t < 0<GOAL>s.SOppSide ((AffineMap.lineMap x y) t) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<VAR>t : R<VAR>ht : t < 0<GOAL>s.SOppSide y ((AffineMap.lineMap x y) t)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<GOAL>{y | s.WSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<GOAL>{y | s.SSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<GOAL>{y | s.WOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<GOAL>{y | s.SOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x : P<VAR>y : P<VAR>hx : x ∈ s<GOAL>s.WOppSide y ((AffineEquiv.pointReflection R x) y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedField R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<VAR>hy : y ∉ s<GOAL>s.SOppSide y ((AffineEquiv.pointReflection R x) y)