ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>y ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x : P<GOAL>affineSegment R x x = {x}
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>f : P →ᵃ[R] P'<VAR>x y : P<GOAL>⇑f '' affineSegment R x y = affineSegment R (f x) (f y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<VAR>v : V<GOAL>(fun x => v +ᵥ x) '' affineSegment R x y = affineSegment R (v +ᵥ x) (v +ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : V<VAR>p : P<GOAL>(fun x => x +ᵥ p) '' affineSegment R x y = affineSegment R (x +ᵥ p) (y +ᵥ p)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y p : P<GOAL>(fun x => p -ᵥ x) '' affineSegment R x y = affineSegment R (p -ᵥ x) (p -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y p : P<GOAL>(fun x => x -ᵥ p) '' affineSegment R x y = affineSegment R (x -ᵥ p) (y -ᵥ p)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>v : V<GOAL>v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : V<VAR>p : P<GOAL>z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>x y z : V<GOAL>y ∈ segment R x z ↔ Wbtw R x y z
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>f : P →ᵃ[R] P'<GOAL>Wbtw R (f x) (f y) (f z)
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>x y z : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>x y z : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>x y z : P<VAR>f : P ≃ᵃ[R] P'<GOAL>Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z
<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>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>AddCommGroup V'<VAR>Module R V'<VAR>AddTorsor V' P'<VAR>x y z : P<VAR>f : P ≃ᵃ[R] P'<GOAL>Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>v : V<GOAL>Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Wbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : V<VAR>p : P<GOAL>Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Wbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Wbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Wbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>v : V<GOAL>Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : V<VAR>p : P<GOAL>Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>p : P<GOAL>Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>Wbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>y ≠ x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>x ≠ y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>y ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>z ≠ y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>y ∈ affineSpan R {x, z}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<GOAL>Wbtw R x y z ↔ Wbtw R z y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<GOAL>Sbtw R x y z ↔ Sbtw R z y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>Wbtw R x x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>Wbtw R x y y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>Wbtw R x y x ↔ y = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬Sbtw R x x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬Sbtw R x y y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : y ≠ x<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : y ≠ z<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<GOAL>Sbtw R x y z ↔ y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>¬Sbtw R x y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y : P<VAR>z : P<GOAL>Wbtw R x y z ∧ Wbtw R y x z ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x : P<VAR>y z : P<GOAL>Wbtw R x y z ∧ Wbtw R x z y ↔ y = z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x : P<VAR>y z : P<GOAL>Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R y x z ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R x z y ↔ y = z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R z x y ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>¬Wbtw R y x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>¬Wbtw R x z y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>¬Wbtw R z x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y : P<VAR>r : R<GOAL>Wbtw R x ((AffineMap.lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>x y : P<VAR>r : R<GOAL>Sbtw R x ((AffineMap.lineMap x y) r) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>NoZeroDivisors R<VAR>x y r : R<GOAL>Wbtw R x (r * (y - x) + x) y ↔ x = y ∨ r ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>NoZeroDivisors R<VAR>x y r : R<GOAL>Sbtw R x (r * (y - x) + x) y ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>x : R<GOAL>Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>x : R<GOAL>Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>x : R<GOAL>Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1
<VAR>R : Type u_1<VAR>OrderedRing R<VAR>x : R<GOAL>Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Wbtw R w x y<GOAL>Wbtw R w x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Wbtw R x y z<GOAL>Wbtw R w y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Sbtw R w x y<GOAL>Sbtw R w x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Sbtw R x y z<GOAL>Sbtw R w y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Sbtw R w y z<VAR>h₂ : Sbtw R w x y<GOAL>Sbtw R w x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Sbtw R w x z<VAR>h₂ : Sbtw R x y z<GOAL>Sbtw R w y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Wbtw R w x y<VAR>h : y ≠ z<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Wbtw R x y z<VAR>h : w ≠ x<GOAL>w ≠ y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Sbtw R w y z<VAR>h₂ : Wbtw R w x y<GOAL>x ≠ z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Sbtw R w x z<VAR>h₂ : Wbtw R x y z<GOAL>w ≠ y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroDivisors R<VAR>NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>h : (Finset.affineCombination R s p) w ∈ affineSpan R {(Finset.affineCombination R s p) w₁, (Finset.affineCombination R s p) w₂}<VAR>i : ι<VAR>his : i ∈ s<VAR>hs : Sbtw R (w₁ i) (w i) (w₂ i)<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<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 z : P<VAR>h : Wbtw R x y z<GOAL>SameRay R (y -ᵥ x) (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>x y z : P<VAR>h : Wbtw R x y z<GOAL>SameRay R (y -ᵥ x) (z -ᵥ 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 z : P<VAR>h : Wbtw R x y z<GOAL>SameRay R (z -ᵥ x) (z -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>LinearOrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<GOAL>Sbtw R (t.points i₁) 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>x y z : P<GOAL>Wbtw R x y z ↔ x = y ∨ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1
<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>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : x ≠ y<GOAL>z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1
<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>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : x ≠ y<GOAL>z ∈ affineSpan 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>x y z : P<GOAL>Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1
<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>x y z : P<VAR>h : Sbtw R x y z<GOAL>z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1
<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>x y z : P<VAR>h : Sbtw R x y z<GOAL>z ∈ affineSpan 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>x y z : P<GOAL>Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1
<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>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : z ≠ y<GOAL>x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1
<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>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : z ≠ y<GOAL>x ∈ affineSpan R {z, 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>x y z : P<GOAL>Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1
<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>x y z : P<VAR>h : Sbtw R x y z<GOAL>x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1
<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>x y z : P<VAR>h : Sbtw R x y z<GOAL>x ∈ affineSpan R {z, 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₁ ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : 0 ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ r₁<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ 0<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : 0 ≤ r₂<GOAL>Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ 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>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₂ ≤ 0<GOAL>Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ 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>w x y z : P<VAR>h₁ : Wbtw R w y z<VAR>h₂ : Wbtw R w x y<GOAL>Wbtw R x y 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>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Wbtw R x y z<GOAL>Wbtw R w 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>w x y z : P<VAR>h₁ : Sbtw R w y z<VAR>h₂ : Sbtw R w x y<GOAL>Sbtw R x y 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>w x y z : P<VAR>h₁ : Sbtw R w x z<VAR>h₂ : Sbtw R x y z<GOAL>Sbtw R w 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>x y z : P<VAR>h : Wbtw R x y z<GOAL>Collinear R {x, y, 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>x y z : P<VAR>h : Collinear R {x, y, z}<GOAL>Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z 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>x y z : P<GOAL>Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ 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>x y : P<GOAL>Wbtw R y x ((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>x y : P<VAR>h : x ≠ y<GOAL>Sbtw R y x ((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>x y : P<GOAL>Wbtw R x (midpoint R x y) 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>x y : P<VAR>h : x ≠ y<GOAL>Sbtw R x (midpoint R x y) 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>h : s.WSameSide x y<VAR>f : P →ᵃ[R] P'<GOAL>(AffineSubspace.map f s).WSameSide (f x) (f 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).WSameSide (f x) (f y) ↔ s.WSameSide 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).SSameSide (f x) (f y) ↔ s.SSameSide 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).WSameSide (f x) (f y) ↔ s.WSameSide 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).SSameSide (f x) (f y) ↔ s.SSameSide 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>h : s.WOppSide x y<VAR>f : P →ᵃ[R] P'<GOAL>(AffineSubspace.map f s).WOppSide (f x) (f y)