ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>hab : a < b<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) ≤ slope f ((AffineMap.lineMap a b) r) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>hab : a < b<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b ≤ slope f a ((AffineMap.lineMap a b) r)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>hab : a < b<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) < slope f ((AffineMap.lineMap a b) r) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>hab : a < b<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b < slope f a ((AffineMap.lineMap a b) r)
<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>Ring R<VAR>Invertible 2<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>a b : P<GOAL>f (midpoint R a b) = midpoint R (f a) (f b)
<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>Ring R<VAR>Invertible 2<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>a b : P<GOAL>f (midpoint R a b) = midpoint R (f a) (f b)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>(AffineEquiv.pointReflection R (midpoint R x y)) x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>(Equiv.pointReflection (midpoint R x y)) x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>midpoint R x y = midpoint R y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>(AffineEquiv.pointReflection R (midpoint R x y)) y = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>(Equiv.pointReflection (midpoint R x y)) y = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>midpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>v v' : V<VAR>p p' : P<GOAL>midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<GOAL>midpoint R x y = z ↔ (AffineEquiv.pointReflection R z) x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>midpoint R ((Equiv.pointReflection x) y) y = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>midpoint R y ((Equiv.pointReflection x) y) = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ : P<GOAL>midpoint R p₁ p₂ -ᵥ p₁ = ⅟2 • (p₂ -ᵥ p₁)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ : P<GOAL>midpoint R p₁ p₂ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₁ -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ : P<GOAL>p₂ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₂ -ᵥ p₁)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ p : P<GOAL>midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>p₁ p₂ p : P<GOAL>p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>v₁ v₂ : V<GOAL>midpoint R v₁ v₂ - v₁ = ⅟2 • (v₂ - v₁)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>v₁ v₂ : V<GOAL>midpoint R v₁ v₂ - v₂ = ⅟2 • (v₁ - v₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>v₁ v₂ : V<GOAL>v₁ - midpoint R v₁ v₂ = ⅟2 • (v₁ - v₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>v₁ v₂ : V<GOAL>v₂ - midpoint R v₁ v₂ = ⅟2 • (v₂ - v₁)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>midpoint R x y = x ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>x = midpoint R x y ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>midpoint R x y = y ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>y = midpoint R x y ↔ x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x x' y y' : P<GOAL>midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y z : P<GOAL>midpoint R x y = z ↔ (Equiv.pointReflection z) x = y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>R' : Type u_6<VAR>Ring R'<VAR>Invertible 2<VAR>Module R' V<VAR>x y : P<GOAL>midpoint R x y = midpoint R' x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x : P<GOAL>midpoint R x x = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>midpoint R x y + midpoint R x y = x + y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>midpoint R 0 (x + y) = midpoint R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>midpoint R x y = ⅟2 • (x + y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x : V<GOAL>midpoint R x (-x) = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x : V<GOAL>midpoint R (-x) x = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>midpoint R (x - y) (x + y) = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>midpoint R (x + y) (x - y) = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Ring R<VAR>Invertible 2<VAR>AddCommGroup E<VAR>Module R E<VAR>Ring R'<VAR>Invertible 2<VAR>AddCommGroup F<VAR>Module R' F<VAR>f : E → F<VAR>h0 : f 0 = 0<VAR>hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)<GOAL>⇑(AddMonoidHom.ofMapMidpoint R R' f h0 hm) = f
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>self : AffineBasis ι k P<GOAL>AffineIndependent k self.toFun
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>self : AffineBasis ι k P<GOAL>affineSpan k (Set.range self.toFun) = ⊤
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b₁ b₂ : AffineBasis ι k P<VAR>h : ⇑b₁ = ⇑b₂<GOAL>b₁ = b₂
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<GOAL>AffineIndependent k ⇑b
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<GOAL>affineSpan k (Set.range ⇑b) = ⊤
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<GOAL>Nonempty ι
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>e : ι ≃ ι'<GOAL>⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>(b.reindex e) i' = b (e.symm i')
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<GOAL>b.reindex (Equiv.refl ι) = b
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>i : ι<VAR>j : { j // j ≠ i }<GOAL>(b.basisOf i) j = b ↑j -ᵥ b i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>e : ι ≃ ι'<VAR>i : ι'<GOAL>(b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>i : ι<GOAL>(b.coord i).linear = -(b.basisOf i).sumCoords
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>e : ι ≃ ι'<VAR>i : ι'<GOAL>(b.reindex e).coord i = b.coord (e.symm i)
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>i : ι<GOAL>(b.coord i) (b i) = 1
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>i j : ι<VAR>h : i ≠ j<GOAL>(b.coord i) (b j) = 0
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>DecidableEq ι<VAR>i j : ι<GOAL>(b.coord i) (b j) = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>w : ι → k<VAR>hw : s.sum w = 1<GOAL>(b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>w : ι → k<VAR>hw : s.sum w = 1<GOAL>(b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>q : P<GOAL>∑ i : ι, (b.coord i) q = 1
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>q : P<GOAL>((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>AddCommGroup V<VAR>Ring k<VAR>Module k V<VAR>Fintype ι<VAR>b : AffineBasis ι k V<VAR>v : V<GOAL>∑ i : ι, (b.coord i) v • b i = v
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Finite ι<VAR>q₁ q₂ : P<VAR>h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂<GOAL>q₁ = q₂
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Subsingleton ι<VAR>i : ι<GOAL>⇑(b.coord i) = 1
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Nontrivial ι<VAR>i : ι<GOAL>Function.Surjective ⇑(b.coord i)
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>q : P<VAR>i : ι<GOAL>b.coords q i = (b.coord i) q
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>v : V<VAR>b : AffineBasis ι k P<GOAL>⇑(v +ᵥ b) = v +ᵥ ⇑b
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>v : V<VAR>b : AffineBasis ι k P<GOAL>(v +ᵥ b).basisOf = b.basisOf
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>i : ι<VAR>v : V<VAR>b : AffineBasis ι k P<GOAL>(v +ᵥ b).coord i = (b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm
<VAR>ι : Type u_1<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>CharZero k<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹
<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>t : Set P<VAR>ht : affineSpan k t = ⊤<GOAL>∃ s ⊆ t, ∃ b, ⇑b = Subtype.val
<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<GOAL>∃ s b, ⇑b = Subtype.val
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_4<VAR>V₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₂<VAR>self : P₁ ≃ᵃL[k] P₂<GOAL>Continuous (↑self).toFun
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_4<VAR>V₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₂<VAR>self : P₁ ≃ᵃL[k] P₂<GOAL>Continuous (↑self).invFun
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<GOAL>Function.Injective ContinuousAffineEquiv.toAffineEquiv
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>⇑↑e = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>⇑(↑e).toEquiv = ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e e' : P₁ ≃ᵃL[k] P₂<VAR>h : ∀ (x : P₁), e x = e' x<GOAL>e = e'
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e e' : P₁ ≃ᵃL[k] P₂<GOAL>e = e' ↔ ∀ (x : P₁), e x = e' x
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>Continuous ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<GOAL>⇑(ContinuousAffineEquiv.refl k P₁) = id
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<VAR>x : P₁<GOAL>(ContinuousAffineEquiv.refl k P₁) x = x
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<GOAL>↑(ContinuousAffineEquiv.refl k P₁) = AffineEquiv.refl k P₁
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>V₁ : Type u_6<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>TopologicalSpace P₁<GOAL>(↑(ContinuousAffineEquiv.refl k P₁)).toEquiv = Equiv.refl P₁
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>(↑e).symm = ↑e.symm
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>(↑e).symm = (↑e.symm).toEquiv
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>p : P₂<GOAL>e (e.symm p) = p
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>p : P₁<GOAL>e.symm (e p) = p
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>p₁ : P₁<VAR>p₂ : P₂<GOAL>e p₁ = p₂ ↔ p₁ = e.symm p₂
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>p₁ p₂ : P₁<GOAL>e p₁ = e p₂ ↔ p₁ = p₂
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>e.symm.symm = e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>x : P₁<GOAL>e.symm.symm x = e x
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>x : P₂<VAR>y : P₁<GOAL>e.symm x = y ↔ x = e y
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>x : P₂<VAR>y : P₁<GOAL>y = e.symm x ↔ e y = x
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>f : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₂<GOAL>⇑f.symm '' s = ⇑f ⁻¹' s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>f : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₁<GOAL>⇑f.symm ⁻¹' s = ⇑f '' s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>Function.Bijective ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>Function.Surjective ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<GOAL>Function.Injective ⇑e
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₁<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddTorsor V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AddTorsor V₂ P₂<VAR>TopologicalSpace P₁<VAR>TopologicalSpace P₂<VAR>e : P₁ ≃ᵃL[k] P₂<VAR>s : Set P₂<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s