Theorem ZFSet.isOrdinal_iff_mem_range_toZFSet

Modification history

2025-11-26 18:08

Mathlib/SetTheory/ZFC/Ordinal.lean

feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals (#26544) …

Added ZFSet.isOrdinal_iff_mem_range_toZFSet View on Github →