Commit 2021-09-15 02:43 23eac53f

View on Github →

chore(*): upgrade to Lean 3.33.0c (#9165) My main goal is to fix various diamonds with sup/inf, see leanprover-community/lean#609. I use lean-master + 1 fixup commit leanprover-community/lean#615.

Estimated changes

Modified leanpkg.toml

Modified src/algebra/ordered_monoid.lean

Modified src/data/bool.lean

Modified src/data/finsupp/lattice.lean

Modified src/data/list/func.lean

Modified src/data/list/intervals.lean

modified theorem list.Ico.filter_le

Modified src/data/list/min_max.lean

Modified src/data/nat/cast.lean

Modified src/data/polynomial/degree/definitions.lean

Modified src/data/rat/cast.lean

Modified src/data/real/nnreal.lean

Modified src/data/string/basic.lean

Modified src/field_theory/separable.lean

Modified src/group_theory/order_of_element.lean

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/measure/lebesgue.lean

Modified src/number_theory/pell.lean

Modified src/order/basic.lean

Modified src/order/bounded_lattice.lean

modified theorem with_bot.coe_max

modified theorem with_bot.coe_min

deleted theorem with_bot.inf_eq_min

deleted theorem with_bot.lattice_eq_DLO

deleted theorem with_bot.sup_eq_max

modified theorem with_top.coe_max

modified theorem with_top.coe_min

deleted theorem with_top.inf_eq_min

deleted theorem with_top.lattice_eq_DLO

deleted theorem with_top.sup_eq_max

Modified src/order/conditionally_complete_lattice.lean

Modified src/order/lattice.lean

added def lattice.to_linear_order

Modified src/tactic/fin_cases.lean

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

Modified src/topology/continuous_function/algebra.lean

Modified src/topology/path_connected.lean