Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-20 15:22 3e683f41

View on Github →

chore(algebra,order): cleanup min / max using the lattice theory

Estimated changes

Modified algebra/default.lean

Renamed algebra/functions.lean to algebra/order_functions.lean

added theorem le_max_iff

deleted theorem le_max_left_iff_true

added theorem le_max_left_of_le

deleted theorem le_max_right_iff_true

added theorem le_max_right_of_le

modified theorem le_min_iff

added theorem max_distrib_of_monotone

modified theorem max_le_iff

added theorem max_le_max

modified theorem max_min_distrib_left

modified theorem max_min_distrib_right

added theorem min_distrib_of_monotone

added theorem min_le_iff

added theorem min_le_left_of_le

added theorem min_le_min

added theorem min_le_right_of_le

added theorem min_lt_iff

modified theorem min_max_distrib_left

modified theorem min_max_distrib_right

Modified data/finset.lean

Modified data/int/basic.lean

Modified data/multiset.lean

Modified data/set/intervals.lean

Modified order/boolean_algebra.lean

deleted theorem lattice.eq_of_sup_eq_inf_eq

deleted theorem lattice.inf_eq_bot_iff_le_compl

deleted theorem lattice.inf_sup_left

deleted theorem lattice.inf_sup_right

deleted theorem lattice.le_sup_inf

deleted theorem lattice.sup_inf_left

deleted theorem lattice.sup_inf_right

Modified order/bounded_lattice.lean

added theorem lattice.inf_eq_bot_iff_le_compl

Modified order/lattice.lean

added theorem lattice.eq_of_sup_eq_inf_eq

added theorem lattice.inf_sup_left

added theorem lattice.inf_sup_right

added theorem lattice.le_sup_inf

added theorem lattice.sup_inf_left

added theorem lattice.sup_inf_right