ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = 2<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p : P<VAR>hs : s₁ ≠ s₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁s₁ : p₁ ∈ s₁<VAR>hp₂s₁ : p₂ ∈ s₁<VAR>hps₁ : p ∈ s₁<VAR>hp₁s₂ : p₁ ∈ s₂<VAR>hp₂s₂ : p₂ ∈ s₂<VAR>hps₂ : p ∈ s₂<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<GOAL>0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ ∨ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<GOAL>0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center < s.radius<GOAL>0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Wbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>h : Collinear ℝ {p₁, p₂, p₃}<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center < s.radius<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>x : P × P × P<VAR>hx12 : x.1 ≠ x.2.1<VAR>hx32 : x.2.2 ≠ x.2.1<GOAL>ContinuousAt (fun y => EuclideanGeometry.angle y.1 y.2.1 y.2.2) x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>V₂ : Type u_3<VAR>P₂ : Type u_4<VAR>NormedAddCommGroup V₂<VAR>InnerProductSpace ℝ V₂<VAR>MetricSpace P₂<VAR>NormedAddTorsor V₂ P₂<VAR>f : P →ᵃⁱ[ℝ] P₂<VAR>p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle (f p₁) (f p₂) (f p₃) = EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ : ↥s<GOAL>EuclideanGeometry.angle ↑p₁ ↑p₂ ↑p₃ = EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>v : V<VAR>p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>v₁ v₂ v₃ : V<VAR>p : P<GOAL>EuclideanGeometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ p : P<GOAL>EuclideanGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>v₁ v₂ v₃ v : V<GOAL>EuclideanGeometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>v v₁ v₂ v₃ : V<GOAL>EuclideanGeometry.angle (v + v₁) (v + v₂) (v + v₃) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>v₁ v₂ v₃ v : V<GOAL>EuclideanGeometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>v v₁ v₂ v₃ : V<GOAL>EuclideanGeometry.angle (v - v₁) (v - v₂) (v - v₃) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>v₁ v₂ v₃ : V<GOAL>EuclideanGeometry.angle (-v₁) (-v₂) (-v₃) = EuclideanGeometry.angle v₁ v₂ v₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p3 p2 p1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>0 ≤ EuclideanGeometry.angle p1 p2 p3
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>EuclideanGeometry.angle p1 p2 p3 ≤ π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₀ p : P<GOAL>EuclideanGeometry.angle p₀ p₀ p = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₀ p : P<GOAL>EuclideanGeometry.angle p p₀ p₀ = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p p₀ : P<VAR>h : p ≠ p₀<GOAL>EuclideanGeometry.angle p p₀ p = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = π<GOAL>EuclideanGeometry.angle p2 p1 p3 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = π<GOAL>EuclideanGeometry.angle p2 p3 p1 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 : P<VAR>p2 p3 p4 : P<VAR>h : EuclideanGeometry.angle p2 p3 p4 = π<GOAL>EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p2 p4
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 : P<VAR>p2 p3 p4 : P<VAR>h : EuclideanGeometry.angle p2 p3 p4 = π<GOAL>EuclideanGeometry.angle p1 p3 p2 + EuclideanGeometry.angle p1 p3 p4 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 p4 p5 : P<VAR>hapc : EuclideanGeometry.angle p1 p5 p3 = π<VAR>hbpd : EuclideanGeometry.angle p2 p5 p4 = π<GOAL>EuclideanGeometry.angle p1 p5 p2 = EuclideanGeometry.angle p3 p5 p4
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = π<GOAL>dist p1 p2 ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = π<GOAL>dist p3 p2 ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = π<GOAL>dist p1 p3 = dist p1 p2 + dist p3 p2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>dist p1 p3 = dist p1 p2 + dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : EuclideanGeometry.angle p1 p2 p3 = 0<GOAL>dist p1 p3 = |dist p1 p2 - dist p3 p2|
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>dist p1 p3 = |dist p1 p2 - dist p3 p2| ↔ EuclideanGeometry.angle p1 p2 p3 = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 : P<VAR>hp1p2 : p1 ≠ p2<GOAL>EuclideanGeometry.angle p1 (midpoint ℝ p1 p2) p2 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<GOAL>EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p1 = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<GOAL>EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p2 = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₃ p₂ p₁ = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : p₂ ≠ p₁<GOAL>EuclideanGeometry.angle p₂ p₁ p₃ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₂ p₁ p₃ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : p₂ ≠ p₁<GOAL>EuclideanGeometry.angle p₃ p₁ p₂ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₃ p₁ p₂ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>EuclideanGeometry.angle p₂ p₃ p₁ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₂ p₃ p₁ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>EuclideanGeometry.angle p₁ p₃ p₂ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>EuclideanGeometry.angle p₁ p₃ p₂ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : EuclideanGeometry.angle p₁ p₂ p₃ = 0<GOAL>Collinear ℝ {p₁, p₂, p₃}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : EuclideanGeometry.angle p₁ p₂ p₃ = π<GOAL>Collinear ℝ {p₁, p₂, p₃}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ ≠ π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>0 < EuclideanGeometry.angle p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>EuclideanGeometry.angle p₁ p₂ p₃ < π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = -1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<GOAL>Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>0 < Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear ℝ {p₁, p₂, p₃}<GOAL>Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0<GOAL>Collinear ℝ {p₁, p₂, p₃}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪p₂ -ᵥ p₁, c -ᵥ midpoint ℝ p₁ p₂⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪(Equiv.pointReflection c) p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ ((Equiv.pointReflection p₂) p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>midpoint ℝ p₁ p₂ ∈ AffineSubspace.perpBisector p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>(↑(AffineSubspace.perpBisector p₁ p₂)).Nonempty
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>(AffineSubspace.perpBisector p₁ p₂).direction = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = dist p₁ p₂ ^ 2 / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c p₁ p₂ : P<GOAL>c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.perpBisector p₂ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>p₂ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>p₁ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>AffineSubspace.perpBisector p p = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>AffineSubspace.perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>AffineSubspace.perpBisector p₁ p₂ ≠ ⊥
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁ : dist p₁ c₁ = dist p₂ c₁<VAR>hc₂ : dist p₁ c₂ = dist p₂ c₂<GOAL>⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>V' : Type u_3<VAR>P' : Type u_4<VAR>NormedAddCommGroup V'<VAR>InnerProductSpace ℝ V'<VAR>MetricSpace P'<VAR>NormedAddTorsor V' P'<VAR>f : P → P'<VAR>h : Isometry f<VAR>p₁ p₂ : P<GOAL>f ⁻¹' ↑(AffineSubspace.perpBisector (f p₁) (f p₂)) = ↑(AffineSubspace.perpBisector p₁ p₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>V' : Type u_3<VAR>P' : Type u_4<VAR>NormedAddCommGroup V'<VAR>InnerProductSpace ℝ V'<VAR>MetricSpace P'<VAR>NormedAddTorsor V' P'<VAR>f : P → P'<VAR>h : Isometry f<VAR>p₁ p₂ : P<GOAL>Set.MapsTo f ↑(AffineSubspace.perpBisector p₁ p₂) ↑(AffineSubspace.perpBisector (f p₁) (f p₂))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<GOAL>dist (s.secondInter p v) s.center = dist p s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter p v ∈ s ↔ p ∈ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<GOAL>s.secondInter p 0 = p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>p' : P<VAR>hp' : p' ∈ AffineSubspace.mk' p (Submodule.span ℝ {v})<GOAL>p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>s.secondInter p (r • v) = s.secondInter p v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter p (-v) = s.secondInter p v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter (s.secondInter p v) v = p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p p' : P<GOAL>s.secondInter p (p' -ᵥ p) = (AffineMap.lineMap p p') (-2 * ⟪p' -ᵥ p, p -ᵥ s.center⟫_ℝ / ⟪p' -ᵥ p, p' -ᵥ p⟫_ℝ)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<GOAL>s.secondInter p₁ (p₂ -ᵥ p₁) ∈ affineSpan ℝ {p₁, p₂}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p p' : P<GOAL>Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p p' : P<VAR>hp : p ∈ s<VAR>hp' : dist p' s.center ≤ s.radius<GOAL>Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : EuclideanGeometry.Sphere P<VAR>p p' : P<VAR>hp : p ∈ s<VAR>hp' : dist p' s.center < s.radius<GOAL>Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>x : E<GOAL>stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiffOn ℝ ⊤ (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<GOAL>ContinuousOn (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}