ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℕ → ℕ →. ℕ<GOAL>(Nat.Partrec' fun v => f v.head v.tail.head) ↔ Partrec₂ f
<VAR>m n : ℕ<VAR>f : Mathlib.Vector ℕ m → Mathlib.Vector ℕ n<GOAL>Nat.Partrec'.Vec f ↔ Computable f
<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<GOAL>dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 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>ι₁ : Type u_3<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>p₁ : ι₁ → P<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_4<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>p₂ : ι₂ → P<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>⟪(s₁.weightedVSub p₁) w₁, (s₂.weightedVSub p₂) w₂⟫_ℝ = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 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>ι : Type u_3<VAR>s : Finset ι<VAR>w₁ w₂ : ι → ℝ<VAR>p : ι → P<VAR>h₁ : ∑ i ∈ s, w₁ i = 1<VAR>h₂ : ∑ i ∈ s, w₂ i = 1<GOAL>let_fun a₁ := (Finset.affineCombination ℝ s p) w₁;
let_fun a₂ := (Finset.affineCombination ℝ s p) w₂;
dist a₁ a₂ * dist a₁ a₂ = (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 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>r : ℝ<VAR>v : V<VAR>p₁ p₂ : P<GOAL>dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = ⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + ⟪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>v : V<VAR>p₁ p₂ : P<VAR>hv : v ≠ 0<VAR>r : ℝ<GOAL>dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪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>s : AffineSubspace ℝ P<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<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>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(AffineSubspace.mk' p s.directionᗮ) = {EuclideanGeometry.orthogonalProjectionFn s 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>EuclideanGeometry.orthogonalProjectionFn 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>EuclideanGeometry.orthogonalProjectionFn s p ∈ AffineSubspace.mk' p s.directionᗮ
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>EuclideanGeometry.orthogonalProjectionFn s p -ᵥ p ∈ s.directionᗮ
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>EuclideanGeometry.orthogonalProjectionFn s p = ↑((EuclideanGeometry.orthogonalProjection s) 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<GOAL>(EuclideanGeometry.orthogonalProjection s).linear = ↑(orthogonalProjection s.direction)
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(AffineSubspace.mk' p s.directionᗮ) = {↑((EuclideanGeometry.orthogonalProjection s) 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((EuclideanGeometry.orthogonalProjection 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((EuclideanGeometry.orthogonalProjection s) p) ∈ AffineSubspace.mk' p s.directionᗮ
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p1 : P<VAR>p2 : P<VAR>hp1 : p1 ∈ s<GOAL>↑((EuclideanGeometry.orthogonalProjection s) p2 -ᵥ ⟨p1, hp1⟩) ∈ s.direction
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p1 : P<VAR>p2 : P<VAR>hp1 : p1 ∈ s<GOAL>↑(⟨p1, hp1⟩ -ᵥ (EuclideanGeometry.orthogonalProjection s) p2) ∈ s.direction
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((EuclideanGeometry.orthogonalProjection s) p) = p ↔ 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : ↥s<GOAL>(EuclideanGeometry.orthogonalProjection s) ↑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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(EuclideanGeometry.orthogonalProjection s) ↑((EuclideanGeometry.orthogonalProjection s) p) = (EuclideanGeometry.orthogonalProjection s) 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 s' : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>Nonempty ↥s'<VAR>HasOrthogonalProjection s.direction<VAR>HasOrthogonalProjection s'.direction<VAR>h : s = s'<VAR>p : P<GOAL>↑((EuclideanGeometry.orthogonalProjection s) p) = ↑((EuclideanGeometry.orthogonalProjection s') 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>dist p ↑((EuclideanGeometry.orthogonalProjection s) p) = 0 ↔ 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∉ s<GOAL>dist p ↑((EuclideanGeometry.orthogonalProjection s) 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>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p ∈ s.directionᗮ
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s.directionᗮ
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(orthogonalProjection s.direction) (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) 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>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>(EuclideanGeometry.orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p1 : P<VAR>p2 : P<VAR>r : ℝ<VAR>hp : p1 ∈ s<GOAL>(EuclideanGeometry.orthogonalProjection s) (r • (p2 -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p2)) +ᵥ p1) = ⟨p1, hp⟩
<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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p1 : P<VAR>p2 : P<VAR>hp1 : p1 ∈ s<GOAL>dist p1 p2 * dist p1 p2 = dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) * dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p2) + dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p2) * dist p2 ↑((EuclideanGeometry.orthogonalProjection s) 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>s : AffineSubspace ℝ P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<VAR>r1 r2 : ℝ<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) = dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖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>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(EuclideanGeometry.reflection s) p = ↑((EuclideanGeometry.orthogonalProjection s) p) -ᵥ p +ᵥ ↑((EuclideanGeometry.orthogonalProjection s) 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 s' : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>Nonempty ↥s'<VAR>HasOrthogonalProjection s.direction<VAR>HasOrthogonalProjection s'.direction<VAR>h : s = s'<VAR>p : P<GOAL>(EuclideanGeometry.reflection s) p = (EuclideanGeometry.reflection s') 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(EuclideanGeometry.reflection s) ((EuclideanGeometry.reflection s) 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<GOAL>(EuclideanGeometry.reflection s).symm = EuclideanGeometry.reflection 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<GOAL>Function.Involutive ⇑(EuclideanGeometry.reflection 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(EuclideanGeometry.reflection s) p = p ↔ 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₁ s₂ : AffineSubspace ℝ P<VAR>Nonempty ↥s₁<VAR>Nonempty ↥s₂<VAR>HasOrthogonalProjection s₁.direction<VAR>HasOrthogonalProjection s₂.direction<VAR>p : P<GOAL>(EuclideanGeometry.reflection s₁) p = (EuclideanGeometry.reflection s₂) p ↔ ↑((EuclideanGeometry.orthogonalProjection s₁) p) = ↑((EuclideanGeometry.orthogonalProjection s₂) 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p₁ p₂ : P<GOAL>dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist ((EuclideanGeometry.reflection s) 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>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<GOAL>dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist 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₁ s₂ : AffineSubspace ℝ P<VAR>Nonempty ↥s₁<VAR>HasOrthogonalProjection s₁.direction<VAR>hle : s₁ ≤ s₂<VAR>p : P<VAR>hp : p ∈ s₂<GOAL>(EuclideanGeometry.reflection 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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>(EuclideanGeometry.reflection s) (v +ᵥ p) = -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 : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p₁ : P<VAR>p₂ : P<VAR>r : ℝ<VAR>hp₁ : p₁ ∈ s<GOAL>(EuclideanGeometry.reflection s) (r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂)) +ᵥ p₁) = -(r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂))) +ᵥ p₁
<VAR>α : Type u<VAR>self : Computability.Encoding α<VAR>x : α<GOAL>self.decode (self.encode x) = some x
<VAR>α : Type u<VAR>e : Computability.Encoding α<GOAL>Function.Injective e.encode
<GOAL>Function.LeftInverse Computability.sectionΓ'Bool Computability.inclusionBoolΓ'
<GOAL>Function.Injective Computability.inclusionBoolΓ'
<VAR>n : PosNum<GOAL>Computability.encodePosNum n ≠ []
<VAR>n : PosNum<GOAL>Computability.decodePosNum (Computability.encodePosNum n) = n
<VAR>n : Num<GOAL>Computability.decodeNum (Computability.encodeNum n) = n
<VAR>n : ℕ<GOAL>Computability.decodeNat (Computability.encodeNat n) = n
<VAR>n : ℕ<GOAL>Computability.unaryDecodeNat (Computability.unaryEncodeNat n) = n
<VAR>b : Bool<GOAL>Computability.decodeBool (Computability.encodeBool b) = b
<VAR>α : Type u<VAR>e : Computability.Encoding α<GOAL>Cardinal.lift.{v, u} #α ≤ Cardinal.lift.{u, v} #(List e.Γ)
<VAR>α : Type u<VAR>e : Computability.Encoding α<VAR>Countable e.Γ<GOAL>#α ≤ ℵ₀
<VAR>α : Type u<VAR>e : Computability.FinEncoding α<GOAL>#α ≤ ℵ₀
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j : J<VAR>U : (TopologicalSpace.Opens ↑↑(F.obj j))ᵒᵖ<GOAL>(F.map (𝟙 j)).c.app U = (TopCat.Presheaf.Pushforward.id (F.obj j).presheaf).inv.app U ≫ (TopCat.Presheaf.pushforwardEq ⋯ (F.obj j).presheaf).hom.app U
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (TopologicalSpace.Opens ↑↑(F.obj j₃))ᵒᵖ<GOAL>(F.map (f ≫ g)).c.app U = (F.map g).c.app U ≫ ((TopCat.Presheaf.pushforward C (F.map g).base).map (F.map f).c).app U ≫ (TopCat.Presheaf.pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>CategoryTheory.Limits.HasColimit F<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)<VAR>j : Jᵒᵖ<GOAL>(AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).obj j = (F.obj (Opposite.unop j)).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).base).obj U))
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>CategoryTheory.Limits.HasColimit F<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)<VAR>j k : Jᵒᵖ<VAR>f : j ⟶ k<GOAL>(AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).map f = (F.map f.unop).c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).base).obj U)) ≫ (F.obj (Opposite.unop k)).presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j : J<GOAL>(AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).obj j = Opposite.op ((TopCat.Presheaf.pushforward C (CategoryTheory.Limits.colimit.ι (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C) j)).obj (F.obj j).presheaf)
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>(AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).map f = ((TopCat.Presheaf.pushforward C (CategoryTheory.Limits.colimit.ι (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C) j')).map (F.map f).c ≫ (TopCat.Presheaf.Pushforward.comp ((F ⋙ AlgebraicGeometry.PresheafedSpace.forget C).map f) (CategoryTheory.Limits.colimit.ι (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C) j') (F.obj j).presheaf).inv ≫ (TopCat.Presheaf.pushforwardEq ⋯ (F.obj j).presheaf).hom).op
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<GOAL>↑(AlgebraicGeometry.PresheafedSpace.colimit F) = CategoryTheory.Limits.colimit (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C)
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<GOAL>(AlgebraicGeometry.PresheafedSpace.colimit F).presheaf = CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j : J<GOAL>((AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j).c = CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp (Opposite.op j)
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<GOAL>(AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt = AlgebraicGeometry.PresheafedSpace.colimit F
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>j : J<GOAL>((AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j).base = CategoryTheory.Limits.colimit.ι (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C) j
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>s : CategoryTheory.Limits.Cocone F<VAR>U V : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ<VAR>i : U ⟶ V<GOAL>s.pt.presheaf.map i ≫ AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s V = AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U ≫ ((TopCat.Presheaf.pushforward C (CategoryTheory.Limits.colimit.desc (F ⋙ AlgebraicGeometry.PresheafedSpace.forget C) ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj (AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt.presheaf).map i
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>s : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>(AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j ≫ AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc F s = s.ι.app j
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)<VAR>j : J<GOAL>(AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (CategoryTheory.Limits.colimit.ι F j).c.app (Opposite.op U) = CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U) (Opposite.op j)
<VAR>J : Type u'<VAR>CategoryTheory.Category.{v', u'} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasColimitsOfShape J TopCat<VAR>∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)<VAR>CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ AlgebraicGeometry.PresheafedSpace C<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)<VAR>j : J<GOAL>(AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U) (Opposite.op j) = (CategoryTheory.Limits.colimit.ι F j).c.app (Opposite.op U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → β<VAR>q : β → Prop<VAR>h : Computable f<GOAL>(fun a => q (f a)) ≤₀ q
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>p ≤₀ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>p ≤₀ q → q ≤₀ r → p ≤₀ r
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Reflexive ManyOneReducible
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Transitive ManyOneReducible