Mathlib v3 is deprecated. Go to Mathlib v4

Theorem strict_mono_restrict

Modification history

2022-11-21 19:57

src/data/set/function.lean

feat(order/modular_lattice): Modular lattices are lower modular (#17403)

Added strict_mono_restrict View on Github →