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 #
OrderDual α
: A type synonym reversing the meaning of all inequalities, with notationαᵒᵈ
.AsLinearOrder α
: A type synonym to promotePartialOrder α
toLinearOrder α
usingIsTotal α (≤)
.
Transferring orders #
Order.Preimage
,Preorder.lift
: Transfers a (pre)order onβ
to an order onα
using a functionf : α → β
.PartialOrder.lift
,LinearOrder.lift
: Transfers a partial (resp., linear) order onβ
to a partial (resp., linear) order onα
using an injective functionf
.
Extra class #
DenselyOrdered
: 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 ≤
(LE.le
) and <
(LT.lt
). To that end, we
provide many aliases to dot notation-less lemmas. For example, le_trans
is aliased with
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 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 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 lt_of_lt_of_le'
.
Alias of le_of_le_of_eq
.
Alias of le_of_le_of_eq'
.
Alias of lt_of_lt_of_eq
.
Alias of lt_of_lt_of_eq'
.
Alias of le_of_eq_of_le
.
Alias of le_of_eq_of_le'
.
Alias of lt_of_eq_of_lt
.
Alias of lt_of_eq_of_lt'
.
Alias of eq_iff_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 gt_or_eq_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.
A symmetric relation implies two values are equal, when it implies they're less-equal.
To prove commutativity of a binary operation ○
, we only to check a ○ b ≤ b ○ a
for all a
,
b
.
To prove associativity of a commutative binary operation ○
, we only to check
(a ○ b) ○ c ≤ a ○ (b ○ c)
for all a
, b
, c
.
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 RelEmbedding
(assuming f
is injective).
Instances For
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 RelEmbedding
(assuming f
is injective).
Equations
- «term_⁻¹'o_» = Lean.ParserDescr.trailingNode `«term_⁻¹'o_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹'o ") (Lean.ParserDescr.cat `term 81))
Instances For
The preimage of a decidable order is decidable.
Equations
- Order.Preimage.decidable f s x✝ x = H (f x✝) (f x)
Perform a case-split on the ordering of x
and y
in a decidable linear order,
non-dependently.
Equations
Instances For
Order dual #
Type synonym to equip a type with the dual order: ≤
means ≥
and <
means >
. αᵒᵈ
is
notation for OrderDual α
.
Equations
- «term_ᵒᵈ» = Lean.ParserDescr.trailingNode `«term_ᵒᵈ» 1024 0 (Lean.ParserDescr.symbol "ᵒᵈ")
Instances For
Equations
- ⋯ = h
Equations
- OrderDual.instLE α = { le := fun (x y : α) => y ≤ x }
Equations
- OrderDual.instLT α = { lt := fun (x y : α) => y < x }
Equations
- OrderDual.instPreorder α = Preorder.mk ⋯ ⋯ ⋯
Equations
Equations
- OrderDual.instLinearOrder α = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE inferInstance ⋯ ⋯ ⋯
The opposite linear order to a given linear order
Equations
Instances For
Order instances on the function space #
Equations
- Pi.preorder = Preorder.mk ⋯ ⋯ ⋯
Equations
- Pi.partialOrder = PartialOrder.mk ⋯
Alias of le_of_strongLT
.
Alias of lt_of_strongLT
.
Alias of strongLT_of_strongLT_of_le
.
Alias of strongLT_of_le_of_strongLT
.
min
/max
recursors #
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 = Preorder.mk ⋯ ⋯ ⋯
Instances For
Transfer a PartialOrder
on β
to a PartialOrder
on α
using an injective
function f : α → β
. See note [reducible non-instances].
Equations
- PartialOrder.lift f inj = PartialOrder.mk ⋯
Instances For
Transfer a LinearOrder
on β
to a LinearOrder
on α
using an injective
function f : α → β
. This version takes [Max α]
and [Min α]
as arguments, then uses
them for max
and min
fields. See LinearOrder.lift'
for a version that autogenerates min
and
max
fields, and LinearOrder.liftWithOrd
for one that does not auto-generate compare
fields. See note [reducible non-instances].
Equations
- LinearOrder.lift f inj hsup hinf = LinearOrder.mk ⋯ (fun (x y : α) => inferInstance) (fun (x y : α) => decidable_of_iff (f x = f y) ⋯) (fun (x y : α) => inferInstance) ⋯ ⋯ ⋯
Instances For
Transfer a LinearOrder
on β
to a LinearOrder
on α
using an injective
function f : α → β
. This version autogenerates min
and max
fields. See LinearOrder.lift
for a version that takes [Max α]
and [Min α]
, then uses them as max
and min
. See
LinearOrder.liftWithOrd'
for a version which does not auto-generate compare
fields.
See note [reducible non-instances].
Equations
- LinearOrder.lift' f inj = LinearOrder.lift f inj ⋯ ⋯
Instances For
Transfer a LinearOrder
on β
to a LinearOrder
on α
using an injective
function f : α → β
. This version takes [Max α]
and [Min α]
as arguments, then uses
them for max
and min
fields. It also takes [Ord α]
as an argument and uses them for compare
fields. See LinearOrder.lift
for a version that autogenerates compare
fields, and
LinearOrder.liftWithOrd'
for one that auto-generates min
and max
fields.
fields. See note [reducible non-instances].
Equations
- LinearOrder.liftWithOrd f inj hsup hinf compare_f = LinearOrder.mk ⋯ (fun (x y : α) => inferInstance) (fun (x y : α) => decidable_of_iff (f x = f y) ⋯) (fun (x y : α) => inferInstance) ⋯ ⋯ ⋯
Instances For
Transfer a LinearOrder
on β
to a LinearOrder
on α
using an injective
function f : α → β
. This version auto-generates min
and max
fields. It also takes [Ord α]
as an argument and uses them for compare
fields. See LinearOrder.lift
for a version that
autogenerates compare
fields, and LinearOrder.liftWithOrd
for one that doesn't auto-generate
min
and max
fields. fields. See note [reducible non-instances].
Equations
- LinearOrder.liftWithOrd' f inj compare_f = LinearOrder.liftWithOrd f inj ⋯ ⋯ compare_f
Instances For
Subtype of an order #
Equations
- Subtype.preorder p = Preorder.lift fun (a : Subtype p) => ↑a
Equations
- Subtype.partialOrder p = PartialOrder.lift (fun (a : Subtype p) => ↑a) ⋯
Equations
- a.decidableLE b = h ↑a ↑b
Equations
- a.decidableLT b = h ↑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.instLinearOrder p = LinearOrder.lift (fun (a : Subtype p) => ↑a) ⋯ ⋯ ⋯
Pointwise order on α × β
#
The lexicographic order is defined in Data.Prod.Lex
, and the instances are available via the
type synonym α ×ₗ β = α × β
.
Equations
- Prod.instPreorder α β = Preorder.mk ⋯ ⋯ ⋯
The pointwise partial order on a product.
(The lexicographic ordering is defined in Order.Lexicographic
, and the instances are
available via the type synonym α ×ₗ β = α × β
.)
Equations
Additional order classes #
Equations
- ⋯ = ⋯
Any ordered subsingleton is densely ordered. Not an instance to avoid a heavy subsingleton typeclass search.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
Linear order from a total partial order #
Type synonym to create an instance of LinearOrder
from a PartialOrder
and IsTotal α (≤)
Equations
- AsLinearOrder α = α
Instances For
Equations
- instInhabitedAsLinearOrder = { default := default }
Equations
- AsLinearOrder.linearOrder = LinearOrder.mk ⋯ (Classical.decRel fun (x1 x2 : AsLinearOrder α) => x1 ≤ x2) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯