English
An equivalent form: i.Maximal holds exactly when given any κ and w, if w ∘ j = v for some j, then j is surjective.
Русский
Эквивалентная форма: i.Maximal истинно тогда и только тогда, когда для любых κ и w, если существует j с w ∘ j = v, тогда j сюрьективно.
LaTeX
$$$i.Maximal \leftrightarrow \forall (\kappa) (w: \kappa \to M) (_i' : LinearIndependent R w) (j : ι \to \kappa) (_h : w \circ j = v), Surjective j$$$
Lean4
theorem linearIndependent_iffₒₛ :
LinearIndependent R v ↔
∀ (s t : Finset ι) (f : ι → R),
Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0 :=
by
classical
letI : Sub R := CanonicallyOrderedAdd.toSub
haveI : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
rw [linearIndependent_iff'ₛ]
refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
· specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
· simpa
refine ⟨fun i hi => ?_, fun i hi => ?_⟩
· simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)
· simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm
· specialize h ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i}) (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
· simp_rw [Finset.disjoint_left, Finset.mem_filter]
exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
· rw [← add_right_cancel_iff (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
convert heq <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le] <;>
congr! 2 with i hi <;>
simp only [Finset.mem_filter] at hi
· simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
· simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
simp only [Finset.mem_filter] at h
intro i hi
by_cases hi' : g i ≤ f i
· apply hi'.antisymm'
simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
· apply (not_le.1 hi').le.antisymm
simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩
