Theorem OrdinalApprox.gfpApprox_anti_right

Modification history

2026-04-05 08:48

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

chore(SetTheory/Ordinal/FixedPointApproximants): simpler definition for `lfpApprox` (#37383) …

Added OrdinalApprox.gfpApprox_anti_right View on Github →