Theorem Ordinal.toZFSet_subset_toZFSet_iff

Modification history

2025-11-26 18:08
Mathlib/SetTheory/ZFC/Ordinal.lean
feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals (#26544) …
Added Ordinal.toZFSet_subset_toZFSet_iffView on Github →