Mathlib.Order.Defs.Unbundled

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

Instances

Order.Preimage.instIsStrictWeakOrder

source

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

Instances

source

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

Instances

source

instance eq_isEquiv (α : Sort u_1) :

IsEquiv α fun (x1 x2 : α) => x1 = x2

Equality is an equivalence relation.

source

instance iff_isEquiv :

IsEquiv Prop Iff

Iff is an equivalence relation.

source

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

¬r a a

source

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

r a a

source

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

r a b → r b c → r a c

source

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

r a b → r b a

source

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

r a b → r b a → a = b

source

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

r a b → ¬r b a

source

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

r a b ∨ a = b ∨ r b a

source

@[instance 90]

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

IsAsymm α r

source

instance IsIrrefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsIrrefl α r] :

IsIrrefl α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsRefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsRefl α r] :

IsRefl α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsTrans.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] :

IsTrans α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsSymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsSymm α r] :

IsSymm α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsAntisymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAntisymm α r] :

IsAntisymm α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsAsymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAsymm α r] :

IsAsymm α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsTotal.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] :

IsTotal α fun (a b : α) => Decidable.decide (r a b) = true

source

instance IsTrichotomous.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrichotomous α r] :

IsTrichotomous α fun (a b : α) => Decidable.decide (r a b) = true

source

@[elab_without_expected_type]

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

¬r a a

source

@[elab_without_expected_type]

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

r a a

source

@[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

source

@[elab_without_expected_type]

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

r a b → r b a

source

@[elab_without_expected_type]

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

r a b → ¬r b a

source

@[elab_without_expected_type]

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

r a b ∨ r b a

source

@[elab_without_expected_type]

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

r a b ∨ a = b ∨ r b a

source

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

Prop

IsRefl as a definition, suitable for use in proofs.

Equations

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

source

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

source

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

source

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

Prop

IsIrrefl as a definition, suitable for use in proofs.

Equations

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

source

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

source

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

source

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

Reflexive r

source

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

Symmetric r

source

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

Transitive r

source

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

Transitive (InvImage r f)

source

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

Irreflexive (InvImage r f)

source

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)

source

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)

source

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

P x

source

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

P x

source

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

source

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

source

def MinimalFor {ι : Sort u_1} {α : Type u_2} [LE α] (P : ι → Prop) (f : ι → α) (i : ι) :

Prop

MinimalFor P f i means that f i is minimal over all i satisfying P.

Equations

MinimalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f j ≤ f i → f i ≤ f j)

source

def MaximalFor {ι : Sort u_1} {α : Type u_2} [LE α] (P : ι → Prop) (f : ι → α) (i : ι) :

Prop

MaximalFor P f i means that f i is maximal over all i satisfying P.

Equations

MaximalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f i ≤ f j → f j ≤ f i)

source

theorem MinimalFor.prop {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i : ι} (h : MinimalFor P f i) :

P i

source

theorem MaximalFor.prop {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i : ι} (h : MaximalFor P f i) :

P i

source

theorem MinimalFor.le_of_le {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i j : ι} (h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) :

f i ≤ f j

source

theorem MaximalFor.le_of_le {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i j : ι} (h : MaximalFor P f i) (hj : P j) (hij : f i ≤ f j) :

f j ≤ f i

source

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

source

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

source

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.

Instances For

source

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.

Instances For

source

def IsRelUpperSet {α : Type u_1} [LE α] (s : Set α) (P : α → Prop) :

Prop

An upper set relative to a predicate P is a set such that all elements satisfy P and any element greater than one of its members and satisfying P is also a member.

Equations

IsRelUpperSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s

source

def IsRelLowerSet {α : Type u_1} [LE α] (s : Set α) (P : α → Prop) :

Prop

A lower set relative to a predicate P is a set such that all elements satisfy P and any element less than one of its members and satisfying P is also a member.

Equations

IsRelLowerSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s

source

structure RelUpperSet {α : Type u_1} [LE α] (P : α → Prop) :

Type u_1

The type of upper sets of an order relative to P.

An upper set relative to a predicate P is a set such that all elements satisfy P and any element greater than one of its members and satisfying P is also a member.

carrier : Set α
The carrier of a RelUpperSet.
isRelUpperSet' : IsRelUpperSet self.carrier P
The carrier of a RelUpperSet is an upper set relative to P.
Do NOT use directly. Please use RelUpperSet.isRelUpperSet instead.

source

structure RelLowerSet {α : Type u_1} [LE α] (P : α → Prop) :

Type u_1

The type of lower sets of an order relative to P.

A lower set relative to a predicate P is a set such that all elements satisfy P and any element less than one of its members and satisfying P is also a member.

carrier : Set α
The carrier of a RelLowerSet.
isRelLowerSet' : IsRelLowerSet self.carrier P
The carrier of a RelLowerSet is a lower set relative to P.
Do NOT use directly. Please use RelLowerSet.isRelLowerSet instead.

source

theorem of_eq {α : Type u_1} {r : α → α → Prop} [IsRefl α r] {a b : α} :

a = b → r a b

source

theorem comm {α : Type u_1} {r : α → α → Prop} [IsSymm α r] {a b : α} :

r a b ↔ r b a

source

theorem antisymm' {α : Type u_1} {r : α → α → Prop} [IsAntisymm α r] {a b : α} :

r a b → r b a → b = a

source

theorem antisymm_iff {α : Type u_1} {r : α → α → Prop} [IsRefl α r] [IsAntisymm α r] {a b : α} :

r a b ∧ r b a ↔ a = b

source

@[elab_without_expected_type]

theorem antisymm_of {α : Type u_1} (r : α → α → Prop) [IsAntisymm α r] {a b : α} :

r a b → r b a → a = b

A version of antisymm with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

source

@[elab_without_expected_type]

theorem antisymm_of' {α : Type u_1} (r : α → α → Prop) [IsAntisymm α r] {a b : α} :

r a b → r b a → b = a

A version of antisymm' with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

source

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

r a b ↔ r b a

A version of comm with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

source

theorem IsAsymm.isAntisymm {α : Type u_1} (r : α → α → Prop) [IsAsymm α r] :

IsAntisymm α r

source

theorem IsAsymm.isIrrefl {α : Type u_1} {r : α → α → Prop} [IsAsymm α r] :

IsIrrefl α r

source

theorem IsTotal.isTrichotomous {α : Type u_1} (r : α → α → Prop) [IsTotal α r] :

IsTrichotomous α r

source

@[instance 100]

instance IsTotal.to_isRefl {α : Type u_1} (r : α → α → Prop) [IsTotal α r] :

IsRefl α r

source

theorem ne_of_irrefl {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {x y : α} :

r x y → x ≠ y

source

theorem ne_of_irrefl' {α : Type u_1} {r : α → α → Prop} [IsIrrefl α r] {x y : α} :

r x y → y ≠ x

source

theorem not_rel_of_subsingleton {α : Type u_1} (r : α → α → Prop) [IsIrrefl α r] [Subsingleton α] (x y : α) :

¬r x y

source

theorem rel_of_subsingleton {α : Type u_1} (r : α → α → Prop) [IsRefl α r] [Subsingleton α] (x y : α) :

r x y

source

@[simp]

theorem empty_relation_apply {α : Type u_1} (a b : α) :

EmptyRelation a b ↔ False

source

instance instIsIrreflEmptyRelation {α : Type u_1} :

IsIrrefl α EmptyRelation

source

theorem rel_congr_left {α : Type u_1} {r : α → α → Prop} [IsSymm α r] [IsTrans α r] {a b c : α} (h : r a b) :

r a c ↔ r b c

source

theorem rel_congr_right {α : Type u_1} {r : α → α → Prop} [IsSymm α r] [IsTrans α r] {a b c : α} (h : r b c) :

r a b ↔ r a c

source

theorem rel_congr {α : Type u_1} {r : α → α → Prop} [IsSymm α r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) :

r a c ↔ r b d

source

theorem trans_trichotomous_left {α : Type u_1} {r : α → α → Prop} [IsTrans α r] [IsTrichotomous α r] {a b c : α} (h₁ : ¬r b a) (h₂ : r b c) :

r a c

source

theorem trans_trichotomous_right {α : Type u_1} {r : α → α → Prop} [IsTrans α r] [IsTrichotomous α r] {a b c : α} (h₁ : r a b) (h₂ : ¬r c b) :

r a c

source

theorem transitive_of_trans {α : Type u_1} (r : α → α → Prop) [IsTrans α r] :

Transitive r

source

theorem extensional_of_trichotomous_of_irrefl {α : Type u_1} (r : α → α → Prop) [IsTrichotomous α r] [IsIrrefl α r] {a b : α} (H : ∀ (x : α), r x a ↔ r x b) :

a = b

In a trichotomous irreflexive order, every element is determined by the set of predecessors.

Documentation

Mathlib.Order.Defs.Unbundled

Orders #

Unbundled classes #

Minimal and maximal #

Upper and lower sets #