English
Adding a new index i to a set s preserves algebraic independence if and only if x_i is transcendental over adjoin of x''s outside s.
Русский
Добавление нового индекса i в множество s сохраняет алгебраическую независимость тогда и только тогда, когда x_i трансцендентно над адъойнтом x''s вне s.
LaTeX
$$$\forall s,i (h : i \notin s),\ AlgebraicIndepOn R x (insert i s) \iff (AlgebraicIndepOn R x s) \land Transcendental (adjoin R (x'' s)) (x i)$$
Lean4
theorem insert_iff {s : Set ι} {i : ι} (h : i ∉ s) :
AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (adjoin R (x '' s)) (x i) :=
by
classical simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm, AlgebraicIndepOn]
convert option_iff (x := fun i : s ↦ x i) (a := x i) using 2
· ext (_ | _) <;> rfl
· rw [Set.image_eq_range]
