Theorem OrdinalApprox.lfpApprox_mono_left

Modification history

2026-04-05 15:16
Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
feat(SetTheory/Ordinal/FixedPointApproximants): add zero and limit lemmas for approximants (#37375) …
Modified OrdinalApprox.lfpApprox_mono_leftView on Github →
2026-04-05 08:48
Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
chore(SetTheory/Ordinal/FixedPointApproximants): simpler definition for `lfpApprox` (#37383) …
Modified OrdinalApprox.lfpApprox_mono_leftView on Github →
2024-09-26 02:42
Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
feat: monotonicity lemmas for OrdinalApprox (#15522) …
Added OrdinalApprox.lfpApprox_mono_leftView on Github →