Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.is_normal.apply_omega

Modification history

2022-02-01 10:02

src/set_theory/ordinal_arithmetic.lean

feat(set_theory/ordinal_arithmetic): Normal functions evaluated at `ω` (#11687)

Added ordinal.is_normal.apply_omega View on Github →