Theorem strictMono_restrict

Modification history

2026-07-20 01:34
Mathlib/Data/Set/Monotone.lean
refactor: rename restrict to domRestrict (#25980) …
Deleted strictMono_restrictView on Github →
2025-06-25 10:16
Mathlib/Data/Set/Monotone.lean
feat(Set/Monotone): convenience special cases for monotonicity on insert (#26369) …
Modified strictMono_restrictView on Github →
2024-10-04 14:05
Mathlib/Data/Set/Function.lean
chore(Data/Set): split Data/Set/Function (#17091) …
Modified strictMono_restrictView on Github →
2022-12-15 04:45
Mathlib/Data/Set/Function.lean
feat: port Data.Set.Function (#1035) …
Added strictMono_restrictView on Github →