algebraicIndependent_of_finite — Mathlib

English

If s ⊆ A is such that every finite t ⊆ s yields algebraic independence of the inclusions t ↪ A, then the inclusion s ↪ A is algebraically independent.

Русский

Если для каждого конечного подмножества t ⊆ s выполняется независимость включений t ↪ A, то включение s ↪ A также алгебраически независимо.

LaTeX

$$$\text{AlgebraicIndependent}_R\bigl((\uparrow) : s \to A\bigr)$ assuming ∀ t ⊆ s, t. Finite → AlgebraicIndependent R ((↑) : t → A)$$

Lean4

theorem algebraicIndependent_of_finite (s : Set A) (H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R ((↑) : t → A)) :
    AlgebraicIndependent R ((↑) : s → A) :=
  algebraicIndependent_subtype.2 fun p hp ↦
    algebraicIndependent_subtype.1 (H _ (mem_supported.1 hp) (Finset.finite_toSet _)) _ (by simp)

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