epsilon_eq_deriv

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.epsilon_eq_deriv

English

The epsilon number ε_o equals the derivative of the map a ↦ ω^a at o.

Русский

Число ε_o равно производной по mапе a ↦ ω^a в точке o.

LaTeX

$$$\varepsilon_o = \mathrm{deriv}(\lambda a.\ ω^a)\ o$$$

Lean4

theorem epsilon_eq_deriv (o : Ordinal) : ε_ o = deriv (fun a ↦ ω ^ a) o := by
  rw [epsilon, ← succ_zero, veblen_succ, veblen_zero]

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

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

Разделы

Аффилиация

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