Theorem DirectLimit.mk_apply

Modification history

2026-04-28 09:23
Mathlib/Order/DirectedInverseSystem.lean
refactor: make `DirectLimit.lift` the simp-normal form of the bundled versions (#38593) …
Added DirectLimit.mk_applyView on Github →