English
There exists t ⊆ s such that affineSpan t = affineSpan s and t is affinely independent.
Русский
Существует подмножество t ⊆ s такое, что оболочка t равна оболочке s и t аффинно независимо.
LaTeX
$$$\\exists t\\subseteq s,\\; \\operatorname{affineSpan}_k(t)=\\operatorname{affineSpan}_k(s) \\land \\operatorname{AffineIndependent} k ((\\uparrow): t\\to P)$$$
Lean4
theorem exists_affineIndependent (s : Set P) :
∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k ((↑) : t → P) :=
by
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
· exact ⟨∅, Set.empty_subset ∅, rfl, affineIndependent_of_subsingleton k _⟩
obtain ⟨b, hb₁, hb₂, hb₃⟩ := exists_linearIndependent k ((Equiv.vaddConst p).symm '' s)
have hb₀ : ∀ v : V, v ∈ b → v ≠ 0 := fun v hv => hb₃.ne_zero (⟨v, hv⟩ : b)
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃
refine ⟨{ p } ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩
· apply Set.union_subset (Set.singleton_subset_iff.mpr hp)
rwa [← (Equiv.vaddConst p).subset_symm_image b s]
· rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂
apply AffineSubspace.ext_of_direction_eq
· have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp
simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]
congr
change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _
rw [Set.image_insert_eq, ← Set.image_comp]
simp
· use p
simp only [Equiv.coe_vaddConst, Set.singleton_union, Set.mem_inter_iff]
exact ⟨mem_affineSpan k (Set.mem_insert p _), mem_affineSpan k hp⟩
