Theorem DirectedOn.insert

Modification history

2023-07-26 08:17

Mathlib/Order/Directed.lean

chore(*): add `protected` to `*.insert` theorems (#6142) …

Deleted DirectedOn.insert View on Github →

2023-04-24 04:16

Mathlib/Order/Directed.lean

feat: forward-port leanprover-community/mathlib#18517 (#2543) …

Added DirectedOn.insert View on Github →