Def Preorder.frestrictLe₂

Modification history

2025-02-27 20:21

Mathlib/Order/Restriction.lean

feat: introduce a predicate `DependsOn` (#22191) …

Modified Preorder.frestrictLe₂ View on Github →

2024-09-16 09:18

Mathlib/Order/Restriction.lean

feat: more definitions for the restriction of a dependent function (#16328) …

Added Preorder.frestrictLe₂ View on Github →