English
If x is algebraically independent over R, and A is nontrivial, then the following are equivalent: the family x restricted to s together with the elements in t is algebraically independent over R, and s and t are disjoint.
Русский
Если x алгебраически независим над R и A не тривиален, то эквивалентны следующие высказывания: независимость x на s вместе с x_i для i∈t над R и неразделимость s и t.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_{R}(x|_s \\cup x|_t) \\iff \\mathrm{Disjoint}(s,t)$$$
Lean4
theorem adjoin_iff_disjoint [Nontrivial A] {s t : Set ι} :
(AlgebraicIndependent (adjoin R (x '' s)) fun i : t ↦ x i) ↔ Disjoint s t :=
by
refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩
have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj
refine ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))
exact ⟨i, hs, rfl⟩
