English
If the sets s and t are linearly independent in their own modules, then the image of s under inl and the image of t under inr form a linearly independent subset of the product M × M'.
Русский
Если множества s и t линейно независимы в своих модулях, то их образы под inl и inr образуют линейно независимое подмножество в произведении M × M'.
LaTeX
$$$\\mathrm{LinearIndepOn}_R(s \\,\text{inl}, t \\,\text{inr})$$$
Lean4
theorem inl_union_inr {s : Set M} {t : Set M'} (hs : LinearIndependent R (fun x => x : s → M))
(ht : LinearIndependent R (fun x => x : t → M')) :
LinearIndependent R (fun x => x : ↥(inl R M M' '' s ∪ inr R M M' '' t) → M × M') :=
by
nontriviality R
let e : s ⊕ t ≃ ↥(inl R M M' '' s ∪ inr R M M' '' t) :=
.ofBijective (Sum.elim (fun i ↦ ⟨_, .inl ⟨_, i.2, rfl⟩⟩) fun i ↦ ⟨_, .inr ⟨_, i.2, rfl⟩⟩)
⟨by rintro (_ | _) (_ | _) eq <;> simp [hs.ne_zero, ht.ne_zero] at eq <;> aesop, by
rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩ <;> aesop⟩
refine (linearIndependent_equiv' e ?_).mp (linearIndependent_inl_union_inr' hs ht)
ext (_ | _) <;> rfl
