cardinalMk_adjoin_le — Mathlib

English

Let F be a field and E an F-algebra, and S a subset of E. Then the intermediate field adjoin F S has cardinality bounded by the supremum of |F|, |S|, and ℵ0: |adjoin F S| ≤ max(|F|, |S|, ℵ0).

Русский

Пусть F — поле, E — дивизиональное расширение над F, и S — подмножество E. Тогда кардинальность промежуточного поля adjoin F S не превышает максимум кардинал |F|, |S| и ℵ0: |adjoin F S| ≤ max(|F|, |S|, ℵ0).

LaTeX

$$$\left| \operatorname{adjoin}_F S \right| \le \max\{ |F|, |S|, \aleph_0 \}$$$

Lean4

theorem cardinalMk_adjoin_le {E : Type u} [Field E] [Algebra F E] (s : Set E) : #(adjoin F s) ≤ #F ⊔ #s ⊔ ℵ₀ := by
  simpa using lift_cardinalMk_adjoin_le F s

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