Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 14:54 b19c491a

View on Github →

chore(order/lattice): rename le_sup_left_of_le (#7856) rename le_sup_left_of_le to le_sup_of_le_left, and variants

Estimated changes

Modified src/algebra/continued_fractions/computation/approximation_corollaries.lean

Modified src/algebra/lie/solvable.lean

Modified src/algebra/order_functions.lean

deleted theorem le_max_left_of_le

added theorem le_max_of_le_left

added theorem le_max_of_le_right

deleted theorem le_max_right_of_le

deleted theorem min_le_left_of_le

added theorem min_le_of_left_le

added theorem min_le_of_right_le

deleted theorem min_le_right_of_le

Modified src/computability/partrec_code.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/data/real/ennreal.lean

Modified src/data/real/nnreal.lean

Modified src/data/set/intervals/basic.lean

Modified src/linear_algebra/finsupp.lean

Modified src/measure_theory/interval_integral.lean

Modified src/number_theory/padics/padic_numbers.lean

Modified src/order/bounds.lean

Modified src/order/complete_lattice.lean

Modified src/order/filter/basic.lean

Modified src/order/lattice.lean

deleted theorem inf_le_left_of_le

added theorem inf_le_of_left_le

added theorem inf_le_of_right_le

deleted theorem inf_le_right_of_le

deleted theorem le_sup_left_of_le

added theorem le_sup_of_le_left

added theorem le_sup_of_le_right

deleted theorem le_sup_right_of_le

Modified src/ring_theory/ideal/over.lean

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/perfection.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/ordered/basic.lean

Modified src/topology/subset_properties.lean