iff_adjoin_image — Mathlib

English

A stronger statement asserting equivalence with a fixed index i, reducing to a unique-element case.

Русский

Усиленное утверждение, эквивалентность через фиксированный индекс i, сводящееся к случаю с уникальным элементом.

LaTeX

$$$\forall (i: ι),\ AlgebraicIndependent R x \iff (AlgebraicIndependent R (fun j => x j) ∧ Transcendental (adjoin R (x '' {i}^c)) (x i))$$

Lean4

theorem iff_adjoin_image (s : Set ι) :
    AlgebraicIndependent R x ↔ AlgebraicIndependent R (fun i : s ↦ x i) ∧ AlgebraicIndepOn (adjoin R (x '' s)) x sᶜ :=
  by
  rw [show x '' s = range fun i : s ↦ x i by ext; simp]
  convert ← sumElim_iff
  classical apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))
  ext (_ | _) <;> rfl

Похожие утверждения