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).
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))
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.
Order dual #
Type synonym to equip a type with the dual order: ≤
means ≥
and <
means >
. αᵒᵈ
is
notation for OrderDual α
.
Instances For
- ComplementedLattice.instOrderDual
- EReal.instLinearOrderedAddCommMonoidWithTopOrderDual
- OrderDual.OrderedCancelAddCommMonoid.to_mulLeftReflectLE
- OrderDual.OrderedCancelCommMonoid.to_mulLeftReflectLE
- OrderDual.addLeftMono
- OrderDual.addLeftReflectLE
- OrderDual.addLeftReflectLT
- OrderDual.addLeftStrictMono
- OrderDual.addRightMono
- OrderDual.addRightReflectLE
- OrderDual.addRightReflectLT
- OrderDual.addRightStrictMono
- OrderDual.borelSpace
- OrderDual.btw
- OrderDual.circularPartialOrder
- OrderDual.circularPreorder
- OrderDual.continuousConstSMul'
- OrderDual.continuousConstVAdd'
- OrderDual.continuousInf
- OrderDual.continuousSup
- OrderDual.denselyOrdered
- OrderDual.finite
- OrderDual.fintype
- OrderDual.infConvergenceClass
- OrderDual.infSet
- OrderDual.instAddArchimedean
- OrderDual.instAddCancelCommMonoid
- OrderDual.instAddCommGroupWithOne
- OrderDual.instAddCommMonoid
- OrderDual.instAddGroup
- OrderDual.instAddGroupWithOne
- OrderDual.instBiheytingAlgebra
- OrderDual.instBooleanAlgebra
- OrderDual.instBornology
- OrderDual.instBot
- OrderDual.instBoundedOrder
- OrderDual.instCancelCommMonoid
- OrderDual.instCircularOrder
- OrderDual.instCoframe
- OrderDual.instCoheytingAlgebra
- OrderDual.instCommMonoid
- OrderDual.instCompleteAtomicBooleanAlgebra
- OrderDual.instCompleteBooleanAlgebra
- OrderDual.instCompleteDistribLattice
- OrderDual.instCompleteLattice
- OrderDual.instCompleteLinearOrder
- OrderDual.instCompletelyDistribLattice
- OrderDual.instConditionallyCompleteLattice
- OrderDual.instConditionallyCompleteLinearOrder
- OrderDual.instDiscreteTopology
- OrderDual.instDistribLattice
- OrderDual.instDistribMulAction
- OrderDual.instDistribMulAction'
- OrderDual.instDistribSMul
- OrderDual.instDistribSMul'
- OrderDual.instDivisionRing
- OrderDual.instDivisionSemiring
- OrderDual.instField
- OrderDual.instFrame
- OrderDual.instGeneralizedCoheytingAlgebra
- OrderDual.instGeneralizedHeytingAlgebra
- OrderDual.instGroup
- OrderDual.instHeytingAlgebra
- OrderDual.instInf
- OrderDual.instInhabited
- OrderDual.instIntCast
- OrderDual.instIsAtomic
- OrderDual.instIsAtomistic
- OrderDual.instIsCoatomic
- OrderDual.instIsCoatomistic
- OrderDual.instIsOrderBornology
- OrderDual.instIsSimpleOrder
- OrderDual.instIsStronglyCoatomic
- OrderDual.instLE
- OrderDual.instLT
- OrderDual.instLattice
- OrderDual.instLinearOrder
- OrderDual.instLocallyFiniteOrder
- OrderDual.instLocallyFiniteOrderBot
- OrderDual.instLocallyFiniteOrderTop
- OrderDual.instMeasurableInf
- OrderDual.instMeasurableInf₂
- OrderDual.instMeasurableSup
- OrderDual.instMeasurableSup₂
- OrderDual.instModule
- OrderDual.instModule'
- OrderDual.instMulActionWithZero
- OrderDual.instMulActionWithZero'
- OrderDual.instMulArchimedean
- OrderDual.instNonempty
- OrderDual.instNontrivial
- OrderDual.instNormedLatticeAddCommGroup
- OrderDual.instOrderBot
- OrderDual.instOrderTop
- OrderDual.instOrderedSMul
- OrderDual.instPartialOrder
- OrderDual.instPosSMulMono
- OrderDual.instPosSMulReflectLE
- OrderDual.instPosSMulReflectLT
- OrderDual.instPosSMulStrictMono
- OrderDual.instPow
- OrderDual.instPow'
- OrderDual.instPreorder
- OrderDual.instRatCast
- OrderDual.instSMul
- OrderDual.instSMul'
- OrderDual.instSMulPosMono
- OrderDual.instSMulPosReflectLE
- OrderDual.instSMulPosReflectLT
- OrderDual.instSMulPosStrictMono
- OrderDual.instSMulWithZero
- OrderDual.instSMulWithZero'
- OrderDual.instSemifield
- OrderDual.instSemilatticeInf
- OrderDual.instSemilatticeSup
- OrderDual.instSubsingleton
- OrderDual.instSup
- OrderDual.instTop
- OrderDual.instTopologicalSpace
- OrderDual.instVAdd
- OrderDual.instVAdd'
- OrderDual.isDirected_ge
- OrderDual.isDirected_le
- OrderDual.isTotal_le
- OrderDual.linearOrderedAddCancelCommMonoid
- OrderDual.linearOrderedAddCommGroup
- OrderDual.linearOrderedAddCommMonoid
- OrderDual.linearOrderedCancelCommMonoid
- OrderDual.linearOrderedCommGroup
- OrderDual.linearOrderedCommMonoid
- OrderDual.mulLeftMono
- OrderDual.mulLeftReflectLE
- OrderDual.mulLeftReflectLT
- OrderDual.mulLeftStrictMono
- OrderDual.mulRightMono
- OrderDual.mulRightReflectLE
- OrderDual.mulRightReflectLT
- OrderDual.mulRightStrictMono
- OrderDual.noBotOrder
- OrderDual.noMaxOrder
- OrderDual.noMinOrder
- OrderDual.noTopOrder
- OrderDual.normedAddCommGroup
- OrderDual.normedAddGroup
- OrderDual.normedCommGroup
- OrderDual.normedGroup
- OrderDual.normedLinearOrderedAddGroup
- OrderDual.normedLinearOrderedGroup
- OrderDual.normedOrderedAddGroup
- OrderDual.normedOrderedGroup
- OrderDual.opensMeasurableSpace
- OrderDual.orderedAddCancelCommMonoid
- OrderDual.orderedAddCommGroup
- OrderDual.orderedAddCommMonoid
- OrderDual.orderedCancelCommMonoid
- OrderDual.orderedCommGroup
- OrderDual.orderedCommMonoid
- OrderDual.sbtw
- OrderDual.seminormedAddCommGroup
- OrderDual.seminormedAddGroup
- OrderDual.seminormedCommGroup
- OrderDual.seminormedGroup
- OrderDual.subtractionCommMonoid
- OrderDual.supConvergenceClass
- OrderDual.supSet
- OrderDual.toNNNorm
- OrderDual.toNorm
- OrderDual.topologicalLattice
- instAddCancelMonoidOrderDual
- instAddCommGroupOrderDual
- instAddCommSemigroupOrderDual
- instAddLeftCancelMonoidOrderDual
- instAddLeftCancelSemigroupOrderDual
- instAddMonoidOrderDual
- instAddOrderDual
- instAddRightCancelMonoidOrderDual
- instAddRightCancelSemigroupOrderDual
- instAddSemigroupOrderDual
- instAddZeroClassOrderDual
- instBornologyOrderDual
- instBoundedGENhdsClassOrderDual
- instBoundedLENhdsClassOrderDual
- instBoundedSpaceOrderDual
- instCancelCommMonoidWithZeroOrderDual
- instCancelMonoidOrderDual
- instCancelMonoidWithZeroOrderDual
- instClosedIciTopologyOrderDual
- instClosedIicTopologyOrderDual
- instCommGroupOrderDual
- instCommGroupWithZeroOrderDual
- instCommMonoidWithZeroOrderDual
- instCommRingOrderDual
- instCommSemigroupOrderDual
- instCommSemiringOrderDual
- instCompactIccSpaceOrderDual
- instContinuousAddOrderDual
- instContinuousConstSMulOrderDual
- instContinuousConstVAddOrderDual
- instContinuousMulOrderDual
- instDistOrderDual
- instDistribOrderDual
- instDivInvMonoidOrderDual
- instDivOrderDual
- instDivisionCommMonoidOrderDual
- instDivisionMonoidOrderDual
- instEDistOrderDual
- instEMetricSpaceOrderDual
- instFirstCountableTopologyOrderDual
- instGroupWithZeroOrderDual
- instHasDistribNegOrderDual
- instInvOrderDual
- instInvolutiveInvOrderDual
- instInvolutiveNegOrderDual
- instIsAddCancelOrderDual
- instIsAddLeftCancelOrderDual
- instIsAddRightCancelOrderDual
- instIsCancelMulOrderDual
- instIsDomainOrderDual
- instIsLeftCancelMulOrderDual
- instIsLowerModularLatticeOrderDual
- instIsModularLatticeOrderDual
- instIsPredArchimedeanOrderDual
- instIsRightCancelMulOrderDual
- instIsStronglyAtomicOrderDualOfIsStronglyCoatomic
- instIsSuccArchimedeanOrderDual
- instIsUpperModularLatticeOrderDual
- instIsWeakLowerModularLatticeOrderDual
- instIsWeakUpperModularLatticeOrderDual
- instLeftCancelMonoidOrderDual
- instLeftCancelSemigroupOrderDual
- instLeftDistribClassOrderDual
- instLipschitzAddOrderDual
- instLipschitzMulOrderDual
- instMeasurableSpaceOrderDual
- instMetricSpaceOrderDual
- instMetricSpaceOrderDual_1
- instMonoidOrderDual
- instMonoidWithZeroOrderDual
- instMulOneClassOrderDual
- instMulOrderDual
- instMulZeroClassOrderDual
- instMulZeroOneClassOrderDual
- instNegOrderDual
- instNoZeroDivisorsOrderDual
- instNonAssocRingOrderDual
- instNonAssocSemiringOrderDual
- instNonUnitalCommRingOrderDual
- instNonUnitalCommSemiringOrderDual
- instNonUnitalNonAssocRingOrderDual
- instNonUnitalNonAssocSemiringOrderDual
- instNonUnitalRingOrderDual
- instNonUnitalSemiringOrderDual
- instOneOrderDual
- instOrderClosedTopologyOrderDual
- instOrderTopologyOrderDual
- instPredOrderOrderDualOfSuccOrder
- instProperSpaceOrderDual
- instPseudoEMetricSpaceOrderDual
- instPseudoMetricSpaceOrderDual
- instPseudoMetricSpaceOrderDual_1
- instRightCancelMonoidOrderDual
- instRightCancelSemigroupOrderDual
- instRightDistribClassOrderDual
- instRingOrderDual
- instSecondCountableTopologyOrderDual
- instSemigroupOrderDual
- instSemigroupWithZeroOrderDual
- instSemiringOrderDual
- instSubNegAddMonoidOrderDual
- instSubOrderDual
- instSubtractionMonoidOrderDual
- instSuccOrderOrderDualOfPredOrder
- instWellFoundedGTOrderDualOfWellFoundedLT
- instWellFoundedLTOrderDualOfWellFoundedGT
- instZeroOrderDual
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 "ᵒᵈ")
Equations
- ⋯ = h
Equations
- OrderDual.instLE α = { le := fun (x y : α) => y ≤ x }
Equations
- OrderDual.instLT α = { lt := fun (x y : α) => y < x }
Equations
- OrderDual.instSup α = { max := fun (x1 x2 : α) => x1 ⊓ x2 }
Equations
- OrderDual.instInf α = { min := fun (x1 x2 : α) => x1 ⊔ x2 }
Equations
- OrderDual.instPreorder α = Preorder.mk ⋯ ⋯ ⋯
Equations
Equations
- OrderDual.instLinearOrder α = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE inferInstance ⋯ ⋯ ⋯
The opposite linear order to a given linear order
Equations
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 ⋯ ⋯ ⋯
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 ⋯
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) ⋯ ⋯ ⋯
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 ⋯ ⋯
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) ⋯ ⋯ ⋯
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
Subtype of an order #
Alias of the reverse direction of Subtype.coe_le_coe
.
Alias of the reverse direction of Subtype.coe_lt_coe
.
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 #
An order is dense if there is an element between any pair of distinct comparable elements.
An order is dense if there is an element between any pair of distinct elements.
Instances
- ENNReal.instDenselyOrdered
- LinearOrderedSemiField.toDenselyOrdered
- NNReal.instDenselyOrdered
- Nonneg.instDenselyOrdered
- NormedField.denselyOrdered_range_nnnorm
- NormedField.denselyOrdered_range_norm
- OrderDual.denselyOrdered
- PUnit.instDenselyOrdered
- Pi.instDenselyOrderedLexForall
- Prod.Lex.instDenselyOrderedLex
- Set.instDenselyOrdered
- Sum.Lex.denselyOrdered_of_noMaxOrder
- Sum.Lex.denselyOrdered_of_noMinOrder
- Sum.denselyOrdered
- WithBot.denselyOrdered
- WithTop.instDenselyOrderedOfNoMaxOrder
- instDenselyOrderedEReal
- instDenselyOrderedForall
- instDenselyOrderedProd
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 ⋯ ⋯ ⋯