ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p2 ∈ s, v = p -ᵥ p2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>p2 -ᵥ p ∈ s.direction ↔ p2 ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>p -ᵥ p2 ∈ s.direction ↔ p2 ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<GOAL>Function.Injective SetLike.coe
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p q : AffineSubspace k P<VAR>h : ∀ (x : P), x ∈ p ↔ x ∈ q<GOAL>p = q
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s₁ s₂ : AffineSubspace k P<GOAL>s₁ = s₂ ↔ ↑s₁ = ↑s₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>hd : s1.direction = s2.direction<VAR>hn : (↑s1 ∩ ↑s2).Nonempty<GOAL>s1 = s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<VAR>a b : ↥s<GOAL>↑(a -ᵥ b) = ↑a -ᵥ ↑b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<VAR>a : ↥s.direction<VAR>b : ↥s<GOAL>↑(a +ᵥ b) = ↑a +ᵥ ↑b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<GOAL>s.subtype.linear = s.direction.subtype
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<VAR>p : ↥s<GOAL>s.subtype p = ↑p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<GOAL>⇑s.subtype = Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>Nonempty ↥s<GOAL>Function.Injective ⇑s.subtype
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s₁ s₂ : AffineSubspace k P<VAR>p : P<VAR>h₁ : p ∈ s₁<VAR>h₂ : p ∈ s₂<GOAL>s₁ = s₂ ↔ s₁.direction = s₂.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>direction : Submodule k V<GOAL>p ∈ AffineSubspace.mk' p direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>p : P<VAR>direction : Submodule k V<VAR>hv : v ∈ direction<GOAL>v +ᵥ p ∈ AffineSubspace.mk' p direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>direction : Submodule k V<GOAL>(↑(AffineSubspace.mk' p direction)).Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>direction : Submodule k V<GOAL>(AffineSubspace.mk' p direction).direction = direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>direction : Submodule k V<GOAL>p₂ ∈ AffineSubspace.mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>AffineSubspace.mk' p s.direction = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>s1 : AffineSubspace k P<VAR>h : s ⊆ ↑s1<GOAL>spanPoints k s ⊆ ↑s1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>p : Submodule k V<VAR>x : V<GOAL>x ∈ p.toAffineSubspace ↔ x ∈ p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>s : Submodule k V<GOAL>s.toAffineSubspace.direction = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Q : AffineSubspace k P<VAR>p₀ p₁ : P<VAR>c : k<VAR>h₀ : p₀ ∈ Q<VAR>h₁ : p₁ ∈ Q<GOAL>(AffineMap.lineMap p₀ p₁) c ∈ Q
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>↑(affineSpan k s) = spanPoints k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>s ⊆ ↑(affineSpan k s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>(affineSpan k s).direction = vectorSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>s : Set P<VAR>hp : p ∈ s<GOAL>p ∈ affineSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1 ≤ s2 ↔ ↑s1 ⊆ ↑s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1 ≤ s2 ↔ ∀ p ∈ s1, p ∈ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1 < s2 ↔ ↑s1 ⊂ ↑s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>¬s1 ≤ s2 ↔ ∃ p ∈ s1, p ∉ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 < s2<GOAL>∃ p ∈ s2, p ∉ s1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s₁ s₂ : AffineSubspace k P<VAR>hd : s₁.direction = s₂.direction<VAR>hn : (↑s₁).Nonempty<VAR>hle : s₁ ≤ s₂<GOAL>s₁ = s₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<GOAL>affineSpan k s = sInf {s' | s ⊆ ↑s'}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>affineSpan k ∅ = ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>affineSpan k Set.univ = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>Q : AffineSubspace k P<GOAL>affineSpan k s ≤ Q ↔ s ⊆ ↑Q
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>p : P<GOAL>↑(affineSpan k {p}) = {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>x : P<GOAL>Subtype.val ⁻¹' {x} = Set.univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s t : Set P<GOAL>affineSpan k (s ∪ t) = affineSpan k s ⊔ affineSpan k t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : ι → Set P<GOAL>affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>↑⊤ = Set.univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>p : P<GOAL>p ∈ ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>⊤.direction = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>↑⊥ = ∅
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>⊥ ≠ ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>h : affineSpan k s = ⊤<GOAL>s.Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>h : affineSpan k s = ⊤<GOAL>vectorSpan k s = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>Nontrivial P<GOAL>affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>Fintype ι<VAR>p : ι → P<VAR>h : affineSpan k (Set.range p) = ⊤<GOAL>0 < Fintype.card ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>(AffineSubspace.topEquiv k V P).linear = (LinearEquiv.ofEq ⊤.direction ⊤ ⋯).trans Submodule.topEquiv
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>a : P<GOAL>↑((AffineSubspace.topEquiv k V P).symm a) = a
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>self : { x // x ∈ Set.univ }<GOAL>(AffineSubspace.topEquiv k V P) self = ↑self
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>p : P<GOAL>p ∉ ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<GOAL>⊥.direction = ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>Q : AffineSubspace k P<GOAL>↑Q = ∅ ↔ Q = ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>Q : AffineSubspace k P<GOAL>↑Q = Set.univ ↔ Q = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>Q : AffineSubspace k P<GOAL>(↑Q).Nonempty ↔ Q ≠ ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>Q : AffineSubspace k P<GOAL>Q = ⊥ ∨ (↑Q).Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<GOAL>Subsingleton P
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<GOAL>s = Set.univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>s.direction = ⊤ ↔ s = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>↑s1 ⊓ ↑s2 = ↑s1 ∩ ↑s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>p : P<VAR>s1 s2 : AffineSubspace k P<GOAL>p ∈ s1 ⊓ s2 ↔ p ∈ s1 ∧ p ∈ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>(s1 ⊓ s2).direction ≤ s1.direction ⊓ s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s₁ s₂ : AffineSubspace k P<VAR>p : P<VAR>h₁ : p ∈ s₁<VAR>h₂ : p ∈ s₂<GOAL>(s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s₁ s₂ : AffineSubspace k P<VAR>p : P<VAR>h : p ∈ s₁ ⊓ s₂<GOAL>(s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 ≤ s2<GOAL>s1.direction ≤ s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 < s2<VAR>hn : (↑s1).Nonempty<GOAL>s1.direction < s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1.direction ⊔ s2.direction ≤ (s1 ⊔ s2).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>he : ↑s1 ∩ ↑s2 = ∅<GOAL>s1.direction ⊔ s2.direction < (s1 ⊔ s2).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : s1.direction ⊔ s2.direction = ⊤<GOAL>(↑s1 ∩ ↑s2).Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>h1 : (↑s1).Nonempty<VAR>h2 : (↑s2).Nonempty<VAR>hd : IsCompl s1.direction s2.direction<GOAL>∃ p, ↑s1 ∩ ↑s2 = {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : AffineSubspace k P<GOAL>affineSpan k ↑s = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>DecidableEq P<VAR>DecidableEq V<VAR>s : Finset P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (s.erase p))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>vectorSpan k (p '' s) = Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i0 : ι<GOAL>vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i0 -ᵥ p i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i0 : ι<GOAL>vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i -ᵥ p i0)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i₀ -ᵥ p ↑i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₀)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>(↑(affineSpan k s)).Nonempty ↔ s.Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>affineSpan k s = ⊥ ↔ s = ∅
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>⊥ < affineSpan k s ↔ s.Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>x : P<VAR>s : Set P<VAR>p : P → Prop<VAR>h : x ∈ affineSpan k s<VAR>mem : ∀ x ∈ s, p x<VAR>smul_vsub_vadd : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)<GOAL>p x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : (x : P) → x ∈ affineSpan k s → Prop<VAR>mem : ∀ (y : P) (hys : y ∈ s), p y ⋯<VAR>smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯<VAR>x : P<VAR>h : x ∈ affineSpan k s<GOAL>p x h
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>A : Set P<VAR>Nonempty ↑A<GOAL>affineSpan k (Subtype.val ⁻¹' A) = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (Set.range Subtype.val) = ⊤<GOAL>affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ p₂ ∈ vectorSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₂ -ᵥ p₁ ∈ vectorSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>r • (p₁ -ᵥ p₂) ∈ vectorSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>r • (p₂ -ᵥ p₁) ∈ vectorSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₁ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₂ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>(AffineMap.lineMap p₁ p₂) r ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>(AffineMap.lineMap p₂ p₁) r ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>r : k<VAR>p₁ p₂ : P<GOAL>r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>affineSpan k {p₁, p₂} ≤ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : p₁ ∈ affineSpan k {p₂, p₃}<GOAL>affineSpan k {p₁, p₃} ≤ affineSpan k {p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : p₁ ∈ affineSpan k {p₂, p₃}<GOAL>affineSpan k {p₂, p₁} ≤ affineSpan k {p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s₁ s₂ : Set P<VAR>h : s₁ ⊆ s₂<GOAL>affineSpan k s₁ ≤ affineSpan k s₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>ps : Set P<GOAL>affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>ps : Set P<VAR>h : p ∈ affineSpan k ps<GOAL>affineSpan k (insert p ps) = affineSpan k ps
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<VAR>ps : Set P<VAR>h : p ∈ affineSpan k ps<GOAL>vectorSpan k (insert p ps) = vectorSpan k ps
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>s : Set V<GOAL>affineSpan k s ≤ (Submodule.span k s).toAffineSubspace
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>s : Set V<GOAL>↑(affineSpan k s) ⊆ ↑(Submodule.span k s)