Orders

Defines classes for preorders, partial orders, and linear orders and proves some basic lemmas about them.

Unbundled classes

def EmptyRelation {α : Sort u_1} : α → α → Prop

An empty relation does not relate any elements.

Equations

• EmptyRelation x✝¹ x✝ = False

class IsIrrefl (α : Sort u_1) (r : α → α → Prop) : Prop

IsIrrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

• irrefl (a : α) : ¬r a a

class IsRefl (α : Sort u_1) (r : α → α → Prop) : Prop

IsRefl X r means the binary relation r on X is reflexive.

• refl (a : α) : r a a

class IsSymm (α : Sort u_1) (r : α → α → Prop) : Prop

IsSymm X r means the binary relation r on X is symmetric.

• symm (a b : α) : r a b → r b a

class IsAsymm (α : Sort u_1) (r : α → α → Prop) : Prop

IsAsymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

• asymm (a b : α) : r a b → ¬r b a

class IsAntisymm (α : Sort u_1) (r : α → α → Prop) : Prop

IsAntisymm X r means the binary relation r on X is antisymmetric.

• antisymm (a b : α) : r a b → r b a → a = b

@[instance 100]

instance IsAsymm.toIsAntisymm {α : Sort u_1} (r : α → α → Prop) [IsAsymm α r] : IsAntisymm α r

class IsTrans (α : Sort u_1) (r : α → α → Prop) : Prop

IsTrans X r means the binary relation r on X is transitive.

• trans (a b c : α) : r a b → r b c → r a c

instance instTransOfIsTrans {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] : Trans r r r

Equations

• instTransOfIsTrans = { trans := ⋯ }

@[instance 100]

instance instIsTransOfTrans {α : Sort u_1} {r : α → α → Prop} [Trans r r r] : IsTrans α r

class IsTotal (α : Sort u_1) (r : α → α → Prop) : Prop

IsTotal X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

• total (a b : α) : r a b ∨ r b a

class IsPreorder (α : Sort u_1) (r : α → α → Prop) extends IsRefl α r, IsTrans α r : Prop

IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c

class IsPartialOrder (α : Sort u_1) (r : α → α → Prop) extends IsPreorder α r, IsAntisymm α r : Prop

IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and IsAntisymm X r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• antisymm (a b : α) : r a b → r b a → a = b

class IsLinearOrder (α : Sort u_1) (r : α → α → Prop) extends IsPartialOrder α r, IsTotal α r : Prop

IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and IsTotal X r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• antisymm (a b : α) : r a b → r b a → a = b
• total (a b : α) : r a b ∨ r b a

class IsEquiv (α : Sort u_1) (r : α → α → Prop) extends IsPreorder α r, IsSymm α r : Prop

IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and IsSymm X r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• symm (a b : α) : r a b → r b a

class IsStrictOrder (α : Sort u_1) (r : α → α → Prop) extends IsIrrefl α r, IsTrans α r : Prop

IsStrictOrder X r means that the binary relation r on X is a strict order, that is, IsIrrefl X r and IsTrans X r.

• irrefl (a : α) : ¬r a a
• trans (a b c : α) : r a b → r b c → r a c

class IsStrictWeakOrder (α : Sort u_1) (lt : α → α → Prop) extends IsStrictOrder α lt : Prop

IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a.

• irrefl (a : α) : ¬lt a a
• trans (a b c : α) : lt a b → lt b c → lt a c
• incomp_trans (a b c : α) : ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

class IsTrichotomous (α : Sort u_1) (lt : α → α → Prop) : Prop

IsTrichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

• trichotomous (a b : α) : lt a b ∨ a = b ∨ lt b a

class IsStrictTotalOrder (α : Sort u_1) (lt : α → α → Prop) extends IsTrichotomous α lt, IsStrictOrder α lt : Prop

IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, IsTrichotomous X lt and IsStrictOrder X lt.

• trichotomous (a b : α) : lt a b ∨ a = b ∨ lt b a
• irrefl (a : α) : ¬lt a a
• trans (a b c : α) : lt a b → lt b c → lt a c

instance eq_isEquiv (α : Sort u_1) : IsEquiv α fun (x1 x2 : α) => x1 = x2

Equality is an equivalence relation.

instance iff_isEquiv : IsEquiv Prop Iff

Iff is an equivalence relation.

theorem irrefl {α : Sort u_1} {r : α → α → Prop} [IsIrrefl α r] (a : α) : ¬r a a

theorem refl {α : Sort u_1} {r : α → α → Prop} [IsRefl α r] (a : α) : r a a

theorem trans {α : Sort u_1} {r : α → α → Prop} {a b c : α} [IsTrans α r] : r a b → r b c → r a c

theorem symm {α : Sort u_1} {r : α → α → Prop} {a b : α} [IsSymm α r] : r a b → r b a

theorem antisymm {α : Sort u_1} {r : α → α → Prop} {a b : α} [IsAntisymm α r] : r a b → r b a → a = b

theorem asymm {α : Sort u_1} {r : α → α → Prop} {a b : α} [IsAsymm α r] : r a b → ¬r b a

theorem trichotomous {α : Sort u_1} {r : α → α → Prop} [IsTrichotomous α r] (a b : α) : r a b ∨ a = b ∨ r b a

@[instance 90]

instance isAsymm_of_isTrans_of_isIrrefl {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [IsIrrefl α r] : IsAsymm α r

instance IsIrrefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsIrrefl α r] : IsIrrefl α fun (a b : α) => decide (r a b) = true

instance IsRefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsRefl α r] : IsRefl α fun (a b : α) => decide (r a b) = true

instance IsTrans.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] : IsTrans α fun (a b : α) => decide (r a b) = true

instance IsSymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsSymm α r] : IsSymm α fun (a b : α) => decide (r a b) = true

instance IsAntisymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAntisymm α r] : IsAntisymm α fun (a b : α) => decide (r a b) = true

instance IsAsymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAsymm α r] : IsAsymm α fun (a b : α) => decide (r a b) = true

instance IsTotal.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] : IsTotal α fun (a b : α) => decide (r a b) = true

instance IsTrichotomous.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrichotomous α r] : IsTrichotomous α fun (a b : α) => decide (r a b) = true

@[elab_without_expected_type]

theorem irrefl_of {α : Sort u_1} (r : α → α → Prop) [IsIrrefl α r] (a : α) : ¬r a a

@[elab_without_expected_type]

theorem refl_of {α : Sort u_1} (r : α → α → Prop) [IsRefl α r] (a : α) : r a a

@[elab_without_expected_type]

theorem trans_of {α : Sort u_1} (r : α → α → Prop) {a b c : α} [IsTrans α r] : r a b → r b c → r a c

@[elab_without_expected_type]

theorem symm_of {α : Sort u_1} (r : α → α → Prop) {a b : α} [IsSymm α r] : r a b → r b a

@[elab_without_expected_type]

theorem asymm_of {α : Sort u_1} (r : α → α → Prop) {a b : α} [IsAsymm α r] : r a b → ¬r b a

@[elab_without_expected_type]

theorem total_of {α : Sort u_1} (r : α → α → Prop) [IsTotal α r] (a b : α) : r a b ∨ r b a

@[elab_without_expected_type]

theorem trichotomous_of {α : Sort u_1} (r : α → α → Prop) [IsTrichotomous α r] (a b : α) : r a b ∨ a = b ∨ r b a

def Reflexive {α : Sort u_1} (r : α → α → Prop) : Prop

IsRefl as a definition, suitable for use in proofs.

Equations

• Reflexive r = ∀ (x : α), r x x

def Symmetric {α : Sort u_1} (r : α → α → Prop) : Prop

IsSymm as a definition, suitable for use in proofs.

Equations

• Symmetric r = ∀ ⦃x y : α⦄, r x y → r y x

def Transitive {α : Sort u_1} (r : α → α → Prop) : Prop

IsTrans as a definition, suitable for use in proofs.

Equations

• Transitive r = ∀ ⦃x y z : α⦄, r x y → r y z → r x z

def Irreflexive {α : Sort u_1} (r : α → α → Prop) : Prop

IsIrrefl as a definition, suitable for use in proofs.

Equations

• Irreflexive r = ∀ (x : α), ¬r x x

def AntiSymmetric {α : Sort u_1} (r : α → α → Prop) : Prop

IsAntisymm as a definition, suitable for use in proofs.

Equations

• AntiSymmetric r = ∀ ⦃x y : α⦄, r x y → r y x → x = y

def Total {α : Sort u_1} (r : α → α → Prop) : Prop

IsTotal as a definition, suitable for use in proofs.

Equations

• Total r = ∀ (x y : α), r x y ∨ r y x

@[deprecated Equivalence.refl (since := "2024-09-13")]

theorem Equivalence.reflexive {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Reflexive r

@[deprecated Equivalence.symm (since := "2024-09-13")]

theorem Equivalence.symmetric {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Symmetric r

@[deprecated Equivalence.trans (since := "2024-09-13")]

theorem Equivalence.transitive {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Transitive r

@[deprecated "No deprecation message was provided." (since := "2024-09-13")]

theorem InvImage.trans {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) (h : Transitive r) : Transitive (InvImage r f)

@[deprecated "No deprecation message was provided." (since := "2024-09-13")]

theorem InvImage.irreflexive {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f)

Minimal and maximal

def Minimal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Minimal P x means that x is a minimal element satisfying P.

Equations

• Minimal P x = (P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x ≤ y)

def Maximal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Maximal P x means that x is a maximal element satisfying P.

Equations

• Maximal P x = (P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → y ≤ x)

theorem Minimal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Minimal P x) : P x

theorem Maximal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Maximal P x) : P x

theorem Minimal.le_of_le {α : Type u_1} [LE α] {P : α → Prop} {x y : α} (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y

theorem Maximal.le_of_ge {α : Type u_1} [LE α] {P : α → Prop} {x y : α} (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x

Upper and lower sets

def IsUpperSet {α : Type u_1} [LE α] (s : Set α) : Prop

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

Equations

• IsUpperSet s = ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s

def IsLowerSet {α : Type u_1} [LE α] (s : Set α) : Prop

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

Equations

• IsLowerSet s = ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s

structure UpperSet (α : Type u_1) [LE α] : Type u_1

The type of upper sets of an order.

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

• carrier : Set α

  The carrier of an UpperSet.

• upper' : IsUpperSet self.carrier

  The carrier of an UpperSet is an upper set.

structure LowerSet (α : Type u_1) [LE α] : Type u_1

The type of lower sets of an order.

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

• carrier : Set α

  The carrier of a LowerSet.

• lower' : IsLowerSet self.carrier

  The carrier of a LowerSet is a lower set.