deg_lt_aleph0

Mathlib.FieldTheory.CardinalEmb

URI: https://scilib.ai/kg/mathlib#Field.Emb.Cardinal.deg_lt_aleph0

English

Reiterates that the degree of X_i is finite for every i: |X_i| < aleph0.

Русский

Повторно утверждается, что для каждого i размер X_i конечен.

LaTeX

$$$$|X_i| < \\aleph_0$$$$

Lean4

theorem deg_lt_aleph0 (i : ι) : #(X i) < ℵ₀ :=
  (toNat_ne_zero.mp (Field.instNeZeroFinSepDegree (E⟮<i⟯) <| E⟮<i⟯⟮b (φ i)⟯).out).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru