cardinalMk_eq — Mathlib

English

If hx and hy are both transcendence bases, then their index cardinalities are equal: #ι = #ι'.

Русский

Если hx и hy являются базисами трансцендентности, то кардиналы их индексов равны: #ι = #ι'.

LaTeX

$$$ (IsTranscendenceBasis R x) \\rightarrow (IsTranscendenceBasis R y) \\rightarrow \\#ι = \\#ι' $$$

Lean4

@[stacks 030F]
theorem cardinalMk_eq {ι' : Type u} {y : ι' → A} (hx : IsTranscendenceBasis R x) (hy : IsTranscendenceBasis R y) :
    #ι = #ι' := by rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]

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