English
Every finite subset of an algebraically independent set is algebraically independent.
Русский
Каждое конечное подмножество алгебраически независимого множества также алгебраически независимо.
LaTeX
$$$\\forall s:\\mathrm{Finset}\,A,\\ (\\text{AlgIndep}_R (i \\mapsto i.val)) \\Rightarrow \\mathrm{AlgIndep}_R (\\text{Subtype}.val)$$$
Lean4
/-- Every finite subset of an algebraically independent set is algebraically independent. -/
theorem algebraicIndependent_finset_map_embedding_subtype (s : Set A) (li : AlgebraicIndependent R ((↑) : s → A))
(t : Finset s) : AlgebraicIndependent R ((↑) : Finset.map (Embedding.subtype s) t → A) :=
by
let f : t.map (Embedding.subtype s) → s := fun x =>
⟨x.1, by
obtain ⟨x, h⟩ := x
rw [Finset.mem_map] at h
obtain ⟨a, _, rfl⟩ := h
simp only [Subtype.coe_prop, Embedding.coe_subtype]⟩
convert AlgebraicIndependent.comp li f _
rintro ⟨x, hx⟩ ⟨y, hy⟩
rw [Finset.mem_map] at hx hy
obtain ⟨a, _, rfl⟩ := hx
obtain ⟨b, _, rfl⟩ := hy
simp only [f, imp_self, Subtype.mk_eq_mk]
