trdeg_eq_iSup_cardinalMk_isTranscendenceBasis

English

The transcendence degree of A over R equals the supremum of the cardinalities of index sets for all transcendence bases of A over R.

Русский

Транцендентный ранг A над R равен наибольшей мощность индексов баз трансцендентности A над R.

LaTeX

$$$\operatorname{trdeg} R A = \big\langle\!\!\!\, ι : { s : Set A // IsTranscendenceBasis R ((↑) : s \to A) } \,, \#ι.1 \!\rangle$$$

Lean4

theorem trdeg_eq_iSup_cardinalMk_isTranscendenceBasis :
    trdeg R A = ⨆ ι : { s : Set A // IsTranscendenceBasis R ((↑) : s → A) }, #ι.1 :=
  by
  refine (ciSup_le' fun s ↦ ?_).antisymm (ciSup_le' fun s ↦ le_ciSup_of_le (bddAbove_range _) ⟨s, s.2.1⟩ le_rfl)
  choose t ht using exists_isTranscendenceBasis_superset s.2
  exact le_ciSup_of_le (bddAbove_range _) ⟨t, ht.2⟩ (mk_le_mk_of_subset ht.1)

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