Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-02 15:24 6392b05a

View on Github →

refactor(*): switch from order_pair to partial_order

Estimated changes

Modified algebra/lattice/basic.lean

modified theorem le_antisymm'

Modified algebra/lattice/bounded_lattice.lean

Modified algebra/lattice/complete_lattice.lean

Modified algebra/lattice/filter.lean

modified theorem directed_of_chain

modified def filter.at_bot

modified def filter.at_top

modified theorem filter.monotone_lift'

modified theorem filter.monotone_lift

modified theorem set.monotone_inter

modified theorem set.monotone_prod

modified theorem set.monotone_set_of

Modified algebra/lattice/fixed_points.lean

modified theorem ge_of_eq

modified theorem lattice.gfp_comp

modified theorem lattice.lfp_comp

Modified algebra/lattice/zorn.lean

added theorem zorn.zorn_partial_order

deleted theorem zorn.zorn_weak_order

Modified algebra/order.lean

modified theorem comp_le_comp_left_of_monotone

modified theorem le_dual_eq_le

modified def weak_order_dual

Modified data/hash_map.lean

Modified data/list/set.lean

Modified data/num/lemmas.lean

Modified data/rat.lean

modified def rat.mk_nat

modified def rat.mk_pnat

Modified data/set/lattice.lean

Modified logic/basic.lean

modified theorem eq_iff_le_and_le

Modified topology/topological_space.lean

Modified topology/uniform_space.lean

modified theorem monotone_comp_rel