Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-21 19:57 124aa163

View on Github →

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

Estimated changes

Modified src/data/set/function.lean

added theorem strict_mono_restrict

Modified src/order/modular_lattice.lean

added def inf_Ioo_order_iso_Ioo_sup

added theorem inf_strict_mono_on_Icc_sup

added theorem sup_strict_mono_on_Icc_inf