algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded

English

If every finite subset of a set is algebraically independent with a bound n, then any set with independence has cardinality at most n.

Русский

Если каждый конечный поднабор обладает независимостью над R и ограничен числом n, то весь набор автономно имеет размер не более n.

LaTeX

$$$\\forall s:\\mathrm{Set}\,A,\\ (\\mathrm{AlgIndep}_R(\\mathrm{Subtype}.val) \\Rightarrow |s| \\le n)$$$

Lean4

/-- If every finite set of algebraically independent element has cardinality at most `n`,
then the same is true for arbitrary sets of algebraically independent elements. -/
theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {n : ℕ}
    (H : ∀ s : Finset A, (AlgebraicIndependent R fun i : s => (i : A)) → s.card ≤ n) :
    ∀ s : Set A, AlgebraicIndependent R ((↑) : s → A) → Cardinal.mk s ≤ n :=
  by
  intro s li
  apply Cardinal.card_le_of
  intro t
  rw [← Finset.card_map (Embedding.subtype s)]
  apply H
  apply algebraicIndependent_finset_map_embedding_subtype _ li

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