Commit 2024-11-26 05:23 b58a5548

View on Github →

chore: split Order.BoundedOrder (#19488)

Estimated changes

Modified Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Associated/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/PSigma/Order.lean

Modified Mathlib/Data/Prod/Lex.lean

Modified Mathlib/Data/Sigma/Order.lean

Renamed Mathlib/Order/BoundedOrder.lean to Mathlib/Order/BoundedOrder/Basic.lean

deleted theorem Antitone.ball

deleted theorem Antitone.exists

deleted theorem Antitone.forall

deleted theorem Monotone.ball

deleted theorem Monotone.exists

deleted theorem Monotone.forall

deleted theorem StrictAnti.apply_eq_bot_iff

deleted theorem StrictAnti.apply_eq_top_iff

deleted theorem StrictMono.apply_eq_bot_iff

deleted theorem StrictMono.apply_eq_top_iff

deleted theorem StrictMono.maximal_preimage_top

deleted theorem StrictMono.minimal_preimage_bot

deleted theorem antitone_le

deleted theorem antitone_lt

deleted theorem bot_inf_eq

deleted theorem bot_sup_eq

deleted theorem exists_and_iff_of_antitone

deleted theorem exists_and_iff_of_monotone

deleted theorem exists_ge_and_iff_exists

deleted theorem exists_le_and_iff_exists

deleted theorem forall_ge_iff

deleted theorem forall_le_iff

deleted theorem inf_bot_eq

deleted theorem inf_eq_top_iff

deleted theorem inf_top_eq

deleted theorem max_bot_left

deleted theorem max_bot_right

deleted theorem max_eq_bot

deleted theorem max_eq_top

deleted theorem max_top_left

deleted theorem max_top_right

deleted theorem min_bot_left

deleted theorem min_bot_right

deleted theorem min_eq_bot

deleted theorem min_eq_top

deleted theorem min_top_left

deleted theorem min_top_right

deleted theorem monotone_and

deleted theorem monotone_le

deleted theorem monotone_lt

deleted theorem monotone_or

deleted theorem sup_bot_eq

deleted theorem sup_eq_bot_iff

deleted theorem sup_top_eq

deleted theorem top_inf_eq

deleted theorem top_sup_eq

Created Mathlib/Order/BoundedOrder/Lattice.lean

added theorem bot_inf_eq

added theorem bot_sup_eq

added theorem exists_and_iff_of_antitone

added theorem exists_and_iff_of_monotone

added theorem exists_ge_and_iff_exists

added theorem exists_le_and_iff_exists

added theorem inf_bot_eq

added theorem inf_eq_top_iff

added theorem inf_top_eq

added theorem max_bot_left

added theorem max_bot_right

added theorem max_eq_bot

added theorem max_eq_top

added theorem max_top_left

added theorem max_top_right

added theorem min_bot_left

added theorem min_bot_right

added theorem min_eq_bot

added theorem min_eq_top

added theorem min_top_left

added theorem min_top_right

added theorem sup_bot_eq

added theorem sup_eq_bot_iff

added theorem sup_top_eq

added theorem top_inf_eq

added theorem top_sup_eq

Created Mathlib/Order/BoundedOrder/Monotone.lean

added theorem Antitone.ball

added theorem Antitone.exists

added theorem Antitone.forall

added theorem Monotone.ball

added theorem Monotone.exists

added theorem Monotone.forall

added theorem StrictAnti.apply_eq_bot_iff

added theorem StrictAnti.apply_eq_top_iff

added theorem StrictMono.apply_eq_bot_iff

added theorem StrictMono.apply_eq_top_iff

added theorem StrictMono.maximal_preimage_top

added theorem StrictMono.minimal_preimage_bot

added theorem antitone_le

added theorem antitone_lt

added theorem forall_ge_iff

added theorem forall_le_iff

added theorem monotone_and

added theorem monotone_le

added theorem monotone_lt

added theorem monotone_or

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Disjoint.lean

Modified Mathlib/Order/Hom/Bounded.lean

Modified Mathlib/Order/Nat.lean

Modified Mathlib/Order/SuccPred/Limit.lean

Modified Mathlib/Order/WithBot.lean

Modified scripts/noshake.json