Mathlib v3 is deprecated. Go to Mathlib v4

Theorem directed_on.insert

Modification history

2023-04-20 11:35
src/order/directed.lean
feat(order/directed): Scott continuous functions (#18517) …
Added directed_on.insertView on Github →