Theorem OrdinalApprox.lfpApprox_mono_right

Modification history

2026-04-05 08:48

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

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

Added OrdinalApprox.lfpApprox_mono_right View on Github →