iff_adjoin_image_compl — Mathlib

English

Specialization of the previous result with a particular i, using a unique-type equivalence.

Русский

Специализация предыдущего результата для конкретного i, с использованием эквивалентности уникального типа.

LaTeX

$$$\forall i,\ AlgebraicIndependent R x \iff (AlgebraicIndependent R (fun j => x j) ∧ Transcendental (Subtype ...) (x i))$$

Lean4

theorem iff_adjoin_image_compl (s : Set ι) :
    AlgebraicIndependent R x ↔ AlgebraicIndependent R (fun i : ↥sᶜ ↦ x i) ∧ AlgebraicIndepOn (adjoin R (x '' sᶜ)) x s :=
  by convert ← iff_adjoin_image _; apply compl_compl

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