exists_isTranscendenceBasis_superset

English

If a subset s of A is algebraically independent over R, there exists a larger set t containing s such that t maps injectively into A and is a transcendence basis of A over R.

Русский

Если множество s ⊆ A алгебраически независимо над R, тогда существует большее множество t ⊇ s, такое что отображение t в A инъективно и является базисом трансцендентности A над R.

LaTeX

$$$\exists t:\ Set A, s \subseteq t \land IsTranscendenceBasis R ((\uparrow) : t \to A)$$$

Lean4

theorem exists_isTranscendenceBasis_superset {s : Set A} (hs : AlgebraicIndepOn R id s) :
    ∃ t, s ⊆ t ∧ IsTranscendenceBasis R ((↑) : t → A) := by
  simpa [← isTranscendenceBasis_iff_maximal] using exists_maximal_algebraicIndependent s _ (subset_univ _) hs

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