aleph0

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.aleph0

English

If for all i, #(f i) = #(g i), then #(Π i, f i) = #(Π i, g i).

Русский

Если для каждого i выполнено #(f i) = #(g i), то #(Π i, f i) = #(Π i, g i).

LaTeX

$$$ \forall {\iota : Type u} {f g : \iota → Type v} (h : \forall i, \#(f i) = #(g i)) : \#(\Pi i, f i) = \#(\Pi i, g i)$$$

Lean4

/-- `ℵ₀` is the smallest infinite cardinal. -/
def aleph0 : Cardinal.{u} :=
  lift #ℕ

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

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

Разделы

Аффилиация

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