Basic definitions about ≤
and <
#
This file proves basic results about orders, provides extensive dot notation, defines useful order classes and allows to transfer order instances.
Type synonyms #
order_dual α
: A type synonym reversing the meaning of all inequalities, with notationαᵒᵈ
.as_linear_order α
: A type synonym to promotepartial_order α
tolinear_order α
usingis_total α (≤)
.
Transfering orders #
order.preimage
,preorder.lift
: Transfers a (pre)order onβ
to an order onα
using a functionf : α → β
.partial_order.lift
,linear_order.lift
: Transfers a partial (resp., linear) order onβ
to a partial (resp., linear) order onα
using an injective functionf
.
Extra class #
densely_ordered
: An order with no gap, i.e. for any two elementsa < b
there existsc
such thata < c < b
.
Notes #
≤
and <
are highly favored over ≥
and >
in mathlib. The reason is that we can formulate all
lemmas using ≤
/<
, and rw
has trouble unifying ≤
and ≥
. Hence choosing one direction spares
us useless duplication. This is enforced by a linter. See Note [nolint_ge] for more infos.
Dot notation is particularly useful on ≤
(has_le.le
) and <
(has_lt.lt
). To that end, we
provide many aliases to dot notation-less lemmas. For example, le_trans
is aliased with
has_le.le.trans
and can be used to construct hab.trans hbc : a ≤ c
when hab : a ≤ b
,
hbc : b ≤ c
, lt_of_le_of_lt
is aliased as has_le.le.trans_lt
and can be used to construct
hab.trans hbc : a < c
when hab : a ≤ b
, hbc : b < c
.
TODO #
- expand module docs
- automatic construction of dual definitions / theorems
Tags #
preorder, order, partial order, poset, linear order, chain
Alias of lt_of_le_of_lt
.
Alias of le_antisymm
.
Alias of ge_antisymm
.
Alias of lt_of_le_of_ne
.
Alias of lt_of_le_of_ne'
.
Alias of lt_of_le_not_le
.
Alias of lt_or_eq_of_le
.
Alias of decidable.lt_or_eq_of_le
.
Alias of lt_of_lt_of_le
.
Alias of le_of_le_of_eq
.
Alias of lt_of_lt_of_eq
.
Alias of le_of_eq_of_le
.
Alias of lt_of_eq_of_lt
.
Alias of not_le_of_lt
.
Alias of not_lt_of_le
.
Alias of decidable.eq_or_lt_of_le
.
Alias of eq_or_lt_of_le
.
Alias of eq_or_gt_of_le
.
Alias of eq_of_le_of_not_lt
.
Alias of eq_of_ge_of_not_gt
.
A version of ne_iff_lt_or_gt
with LHS and RHS reversed.
Given a relation R
on β
and a function f : α → β
, the preimage relation on α
is defined
by x ≤ y ↔ f x ≤ f y
. It is the unique relation on α
making f
a rel_embedding
(assuming f
is injective).
The preimage of a decidable order is decidable.
Equations
- order.preimage.decidable f s = λ (x y : α), H (f x) (f y)
Order dual #
Type synonym to equip a type with the dual order: ≤
means ≥
and <
means >
. αᵒᵈ
is
notation for order_dual α
.
Instances for order_dual
- order_dual.has_measurable_sup
- order_dual.has_measurable_inf
- order_dual.has_measurable_sup₂
- order_dual.has_measurable_inf₂
- order_dual.has_continuous_sup
- order_dual.has_continuous_inf
- order_dual.topological_lattice
- order_dual.normed_group
- order_dual.normed_lattice_add_comm_group
- order_dual.opens_measurable_space
- order_dual.borel_space
- order_dual.nonempty
- order_dual.subsingleton
- order_dual.has_le
- order_dual.has_lt
- order_dual.has_zero
- order_dual.preorder
- order_dual.partial_order
- order_dual.linear_order
- order_dual.inhabited
- order_dual.densely_ordered
- order_dual.nontrivial
- order_dual.no_bot_order
- order_dual.no_top_order
- order_dual.no_min_order
- order_dual.no_max_order
- order_dual.is_total_le
- gt.is_well_order
- has_lt.lt.is_well_order
- order_dual.has_sup
- order_dual.has_inf
- order_dual.semilattice_sup
- order_dual.semilattice_inf
- order_dual.lattice
- order_dual.distrib_lattice
- order_dual.has_top
- order_dual.has_bot
- order_dual.order_top
- order_dual.order_bot
- order_dual.bounded_order
- is_complemented.order_dual.is_complemented
- order_dual.boolean_algebra
- order_dual.has_mul
- order_dual.has_add
- order_dual.has_one
- order_dual.semigroup
- order_dual.add_semigroup
- order_dual.comm_semigroup
- order_dual.add_comm_semigroup
- order_dual.mul_one_class
- order_dual.add_zero_class
- order_dual.monoid
- order_dual.add_monoid
- order_dual.comm_monoid
- order_dual.add_comm_monoid
- order_dual.left_cancel_monoid
- order_dual.left_cancel_add_monoid
- order_dual.right_cancel_monoid
- order_dual.right_cancel_add_monoid
- order_dual.cancel_monoid
- order_dual.cancel_add_monoid
- order_dual.cancel_comm_monoid
- order_dual.cancel_add_comm_monoid
- order_dual.mul_zero_class
- order_dual.mul_zero_one_class
- order_dual.monoid_with_zero
- order_dual.comm_monoid_with_zero
- order_dual.cancel_comm_monoid_with_zero
- order_dual.contravariant_class_mul_le
- order_dual.contravariant_class_add_le
- order_dual.covariant_class_mul_le
- order_dual.covariant_class_add_le
- order_dual.contravariant_class_swap_mul_le
- order_dual.contravariant_class_swap_add_le
- order_dual.covariant_class_swap_mul_le
- order_dual.covariant_class_swap_add_le
- order_dual.contravariant_class_mul_lt
- order_dual.contravariant_class_add_lt
- order_dual.covariant_class_mul_lt
- order_dual.covariant_class_add_lt
- order_dual.contravariant_class_swap_mul_lt
- order_dual.contravariant_class_swap_add_lt
- order_dual.covariant_class_swap_mul_lt
- order_dual.covariant_class_swap_add_lt
- order_dual.ordered_comm_monoid
- order_dual.ordered_add_comm_monoid
- order_dual.ordered_cancel_comm_monoid.to_contravariant_class
- ordered_cancel_add_comm_monoid.to_contravariant_class
- order_dual.ordered_cancel_comm_monoid
- order_dual.ordered_cancel_add_comm_monoid
- order_dual.linear_ordered_cancel_comm_monoid
- order_dual.linear_ordered_cancel_add_comm_monoid
- order_dual.linear_ordered_comm_monoid
- order_dual.linear_ordered_add_comm_monoid
- order_dual.has_inv
- order_dual.has_neg
- order_dual.has_div
- order_dual.has_sub
- order_dual.has_involutive_inv
- order_dual.has_involutive_neg
- order_dual.div_inv_monoid
- order_dual.sub_neg_add_monoid
- order_dual.division_monoid
- order_dual.subtraction_monoid
- order_dual.division_comm_monoid
- order_dual.subtraction_comm_monoid
- order_dual.group
- order_dual.add_group
- order_dual.comm_group
- order_dual.add_comm_group
- order_dual.group_with_zero
- order_dual.comm_group_with_zero
- order_dual.ordered_comm_group
- order_dual.ordered_add_comm_group
- order_dual.linear_ordered_comm_group
- order_dual.linear_ordered_add_comm_group
- order_dual.distrib
- order_dual.has_distrib_neg
- order_dual.non_unital_non_assoc_semiring
- order_dual.non_unital_semiring
- order_dual.non_assoc_semiring
- order_dual.semiring
- order_dual.non_unital_comm_semiring
- order_dual.comm_semiring
- order_dual.non_unital_non_assoc_ring
- order_dual.non_unital_ring
- order_dual.non_assoc_ring
- order_dual.ring
- order_dual.non_unital_comm_ring
- order_dual.comm_ring
- order_dual.has_Sup
- order_dual.has_Inf
- order_dual.complete_lattice
- order_dual.complete_linear_order
- order_dual.is_directed_ge
- order_dual.is_directed_le
- order_dual.coframe
- order_dual.frame
- order_dual.complete_distrib_lattice
- order_dual.fintype
- order_dual.is_modular_lattice
- is_atomic.is_coatomic_dual
- is_coatomic.is_coatomic
- is_atomistic.is_coatomistic_dual
- is_coatomistic.is_atomistic_dual
- order_dual.is_simple_order
- order_dual.conditionally_complete_lattice
- order_dual.conditionally_complete_linear_order
- order_dual.locally_finite_order
- order_dual.locally_finite_order_bot
- order_dual.locally_finite_order_top
- order_dual.pred_order
- order_dual.succ_order
- order_dual.is_pred_archimedean
- order_dual.is_succ_archimedean
- order_dual.archimedean
- order_dual.topological_space
- order_dual.topological_space.first_countable_topology
- order_dual.topological_space.second_countable_topology
- order_dual.has_continuous_mul
- order_dual.has_continuous_add
- order_dual.order_closed_topology
- order_dual.order_topology
- order_dual.has_scalar
- order_dual.smul_with_zero
- order_dual.mul_action
- order_dual.mul_action_with_zero
- order_dual.distrib_mul_action
- order_dual.ordered_smul
- order_dual.module
- order_dual.Sup_convergence_class
- order_dual.Inf_convergence_class
- order_dual.nonempty_fin_lin_ord
- order_dual.measurable_space
- order_dual.has_btw
- order_dual.has_sbtw
- order_dual.circular_preorder
- order_dual.circular_partial_order
- order_dual.circular_order
- order_dual.grade_order
- order_dual.grade_min_order
- order_dual.grade_max_order
- order_dual.grade_bounded_order
Equations
- order_dual.has_le α = {le := λ (x y : α), y ≤ x}
Equations
- order_dual.has_lt α = {lt := λ (x y : α), y < x}
Equations
- order_dual.has_zero α = {zero := 0}
Equations
- order_dual.preorder α = {le := has_le.le (order_dual.has_le α), lt := has_lt.lt (order_dual.has_lt α), le_refl := _, le_trans := _, lt_iff_le_not_le := _}
Equations
- order_dual.partial_order α = {le := preorder.le (order_dual.preorder α), lt := preorder.lt (order_dual.preorder α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- order_dual.linear_order α = {le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := infer_instance (λ (a b : α), has_le.le.decidable b a), decidable_eq := decidable_eq_of_decidable_le infer_instance, decidable_lt := infer_instance (λ (a b : α), has_lt.lt.decidable b a), max := linear_order.min _inst_1, max_def := _, min := linear_order.max _inst_1, min_def := _}
Equations
Order instances on the function space #
Equations
- pi.partial_order = {le := preorder.le pi.preorder, lt := preorder.lt pi.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Lifts of order instances #
Transfer a preorder
on β
to a preorder
on α
using a function f : α → β
.
See note [reducible non-instances].
Equations
- preorder.lift f = {le := λ (x y : α), f x ≤ f y, lt := λ (x y : α), f x < f y, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
Transfer a partial_order
on β
to a partial_order
on α
using an injective
function f : α → β
. See note [reducible non-instances].
Equations
- partial_order.lift f inj = {le := preorder.le (preorder.lift f), lt := preorder.lt (preorder.lift f), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Transfer a linear_order
on β
to a linear_order
on α
using an injective
function f : α → β
. See note [reducible non-instances].
Equations
- linear_order.lift f inj = {le := partial_order.le (partial_order.lift f inj), lt := partial_order.lt (partial_order.lift f inj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (x y : α), infer_instance, decidable_eq := λ (x y : α), decidable_of_iff (f x = f y) _, decidable_lt := λ (x y : α), infer_instance, max := max_default (λ (a b : α), infer_instance), max_def := _, min := min_default (λ (a b : α), infer_instance), min_def := _}
Subtype of an order #
Equations
Equations
Equations
- subtype.decidable_le = λ (a b : subtype p), decidable_of_iff (↑a ≤ ↑b) _
Equations
- subtype.decidable_lt = λ (a b : subtype p), decidable_of_iff (↑a < ↑b) _
A subtype of a linear order is a linear order. We explicitly give the proofs of decidable equality and decidable order in order to ensure the decidability instances are all definitionally equal.
Equations
- subtype.linear_order p = {le := linear_order.le (linear_order.lift coe subtype.coe_injective), lt := linear_order.lt (linear_order.lift coe subtype.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := subtype.decidable_le p, decidable_eq := subtype.decidable_eq (λ (a b : α), eq.decidable a b), decidable_lt := subtype.decidable_lt p, max := linear_order.max (linear_order.lift coe subtype.coe_injective), max_def := _, min := linear_order.min (linear_order.lift coe subtype.coe_injective), min_def := _}
Pointwise order on α × β
#
The lexicographic order is defined in data.prod.lex
, and the instances are available via the
type synonym α ×ₗ β = α × β
.
The pointwise partial order on a product.
(The lexicographic ordering is defined in order/lexicographic.lean, and the instances are
available via the type synonym α ×ₗ β = α × β
.)
Equations
- prod.partial_order α β = {le := preorder.le (prod.preorder α β), lt := preorder.lt (prod.preorder α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Additional order classes #
An order is dense if there is an element between any pair of distinct elements.
Instances of this typeclass
- linear_ordered_field.to_densely_ordered
- order_dual.densely_ordered
- with_bot.densely_ordered
- with_top.densely_ordered
- set.densely_ordered
- sum.densely_ordered
- sum.lex.densely_ordered_of_no_max_order
- sum.lex.densely_ordered_of_no_min_order
- nonneg.densely_ordered
- nnreal.densely_ordered
- ennreal.densely_ordered
- irrational.subtype.densely_ordered
Linear order from a total partial order #
Type synonym to create an instance of linear_order
from a partial_order
and
is_total α (≤)
Equations
- as_linear_order α = α
Instances for as_linear_order
Equations
- as_linear_order.inhabited = {default := inhabited.default _inst_1}
Equations
- as_linear_order.linear_order = {le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le), max := max_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), max_def := _, min := min_default (λ (a b : as_linear_order α), classical.dec_rel has_le.le a b), min_def := _}