def LE.le_rel {α : Type u_1} [LE α] : Relation α α

Equations

• LE.le_rel (a, b) = (a ≤ b)

def LT.lt_rel {α : Type u_1} [LT α] : Relation α α

Equations

• LT.lt_rel (a, b) = (a < b)

@[simp]

theorem LE.mem_le_rel_iff {α : Type u_1} [LE α] {a b : α} : (a, b) ∈ LE.le_rel ↔ a ≤ b

@[simp]

theorem LT.mem_lt_rel_iff {α : Type u_1} [LT α] {a b : α} : (a, b) ∈ LT.lt_rel ↔ a < b

def WithEq (α : Type u_2) : Type u_2

type synonym to use the equality relation as a partial order

Equations

• WithEq α = α

class IsPreorder {α : Type u_1} (r : Relation α α) : Prop

• le_refl : ∀ (a : α), (a, a) ∈ r
• le_trans : ∀ (a b c : α), (a, b) ∈ r → (b, c) ∈ r → (a, c) ∈ r

class IsPartialOrder {α : Type u_1} (r : Relation α α) extends IsPreorder r : Prop

• le_refl : ∀ (a : α), (a, a) ∈ r
• le_trans : ∀ (a b c : α), (a, b) ∈ r → (b, c) ∈ r → (a, c) ∈ r
• le_antisymm : ∀ (a b : α), (a, b) ∈ r → (b, a) ∈ r → a = b

class Preorder (α : Type u_2) extends LE α, LT α : Type u_2

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem Preorder.isPreorder {α : Type u_1} [Preorder α] : IsPreorder {p : α × α | p.fst ≤ p.snd}

class PartialOrder (α : Type u_2) extends Preorder α : Type u_2

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

theorem PartialOrder.isPartialOrder {α : Type u_1} [PartialOrder α] : IsPartialOrder {p : α × α | p.fst ≤ p.snd}

instance instPreorderRelAsLEOfIsPreorder {α : Type u_1} {r : Relation α α} [inst : IsPreorder r] : Preorder (RelAsLE r)

Equations

• instPreorderRelAsLEOfIsPreorder = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderRelAsLEOfIsPartialOrder {α : Type u_1} {r : Relation α α} [inst : IsPartialOrder r] : PartialOrder (RelAsLE r)

Equations

• instPartialOrderRelAsLEOfIsPartialOrder = PartialOrder.mk ⋯

instance instIsPreorderOfIsEquivalence {α : Type u_1} {r : Relation α α} [inst : r.IsEquivalence] : IsPreorder r

Equations

• ⋯ = ⋯

instance instLESubtype_bourbakiLean2 {α : Type u_1} [LE α] {p : α → Prop} : LE { x : α // p x }

Equations

• instLESubtype_bourbakiLean2 = { le := fun (x y : { x : α // p x }) => x.val ≤ y.val }

@[simp]

theorem Subtype.le_iff_val {α : Type u_1} [LE α] {p : α → Prop} {x y : { x : α // p x }} : x ≤ y ↔ x.val ≤ y.val

instance instLTSubtype_bourbakiLean2 {α : Type u_1} [LT α] {p : α → Prop} : LT { x : α // p x }

Equations

• instLTSubtype_bourbakiLean2 = { lt := fun (x y : { x : α // p x }) => x.val < y.val }

@[simp]

theorem Subtype.lt_iff_val {α : Type u_1} [LT α] {p : α → Prop} {x y : { x : α // p x }} : x < y ↔ x.val < y.val

instance instPreorderSubtype {α : Type u_1} [Preorder α] {p : α → Prop} : Preorder { x : α // p x }

Equations

• instPreorderSubtype = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderSubtype {α : Type u_1} [PartialOrder α] {p : α → Prop} : PartialOrder { x : α // p x }

Equations

• instPartialOrderSubtype = PartialOrder.mk ⋯

theorem le_refl {α : Type u_1} [Preorder α] (a : α) : a ≤ a

The relation ≤ on a preorder is reflexive.

@[simp]

theorem le_rfl {α : Type u_1} [Preorder α] {a : α} : a ≤ a

A version of le_refl where the argument is implicit

theorem le_of_eq {α : Type u_1} [Preorder α] {a b : α} (h : a = b) : a ≤ b

theorem le_trans {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u_1} [Preorder α] {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem lt_of_le_not_le {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) (hba : ¬b ≤ a) : a < b

theorem le_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : a ≤ b

theorem ne_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : a ≠ b

theorem not_lt_self {α : Type u_1} [Preorder α] {a : α} : ¬a < a

instance opPreorder {α : Type u_1} [Preorder α] : Preorder (Op α)

Equations

• opPreorder = Preorder.mk ⋯ ⋯ ⋯

def Preorder.equivalent_rel {α : Type u_1} [Preorder α] : Relation α α

Equations

• Preorder.equivalent_rel (a, b) = (a ≤ b ∧ b ≤ a)

@[simp]

theorem Preorder.mem_equivalent_rel_iff {α : Type u_1} [Preorder α] {a b : α} : (a, b) ∈ Preorder.equivalent_rel ↔ a ≤ b ∧ b ≤ a

instance equivalent_rel {α : Type u_1} [Preorder α] : Preorder.equivalent_rel.IsEquivalence

Equations

• ⋯ = ⋯

@[simp]

theorem Preorder.diag_subset_graph {α : Type u_1} [Preorder α] : Relation.diag ⊆ LE.le_rel

@[simp]

theorem Preorder.graph_comp_self {α : Type u_1} [Preorder α] : LE.le_rel.comp LE.le_rel = LE.le_rel

def Preorder.QuotEquiv (α : Type u) [inst : Preorder α] : Type u

Equations

• Preorder.QuotEquiv α = Quot (Function.curry Preorder.equivalent_rel)

def Preorder.QuotEquiv.from {α : Type u} [Preorder α] (h : Preorder.QuotEquiv α) : Quot (Function.curry Preorder.equivalent_rel)

Equations

• h.from = h

def Preorder.QuotEquiv.to {α : Type u} [Preorder α] (h : Quot (Function.curry Preorder.equivalent_rel)) : Preorder.QuotEquiv α

Equations

• Preorder.QuotEquiv.to h = h

def Preorder.QuotEquiv.mk {α : Type u} [Preorder α] (h : α) : Preorder.QuotEquiv α

Equations

• Preorder.QuotEquiv.mk h = Quot.mk (Function.curry Preorder.equivalent_rel) h

def Preorder.carry_bij {α : Type u_1} [Preorder α] {β : Type u_2} (f : Function.Bijection α β) : Preorder β

Equations

• Preorder.carry_bij f = Preorder.mk ⋯ ⋯ ⋯

theorem isPreorder_of_graph_prop {α : Type u_1} {r : Relation α α} (h : r.comp r = r) (h' : Relation.diag ⊆ r) : IsPreorder r

theorem le_antisymm_iff {α : Type u_1} [inst : PartialOrder α] {a b : α} : a ≤ b ∧ b ≤ a ↔ a = b

theorem le_antisymm {α : Type u_1} [inst : PartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b

theorem le_iff_lt_or_eq {α : Type u_1} [inst : PartialOrder α] {a b : α} : a ≤ b ↔ a < b ∨ a = b

theorem lt_iff_le_not_eq {α : Type u_1} [inst : PartialOrder α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b

theorem lt_of_lt_lt {α : Type u_1} [inst : PartialOrder α] {a b c : α} (h : a < b) (h' : b < c) : a < c

theorem lt_of_le_lt {α : Type u_1} [inst : PartialOrder α] {a b c : α} (h : a ≤ b) (h' : b < c) : a < c

theorem lt_of_lt_le {α : Type u_1} [inst : PartialOrder α] {a b c : α} (h : a < b) (h' : b ≤ c) : a < c

def PartialOrder.carry_bij {α : Type u_1} [inst : PartialOrder α] {β : Type u_2} (f : Function.Bijection α β) : PartialOrder β

Equations

• PartialOrder.carry_bij f = PartialOrder.mk ⋯

@[simp]

theorem PartialOrder.equivalent_rel_diag {α : Type u_1} [inst : PartialOrder α] : Preorder.equivalent_rel = Relation.diag

@[simp]

theorem PartialOrder.graph_inter_inv {α : Type u_1} [inst : PartialOrder α] : LE.le_rel ∩ LE.le_rel.inv = Relation.diag

theorem isPartialOrder_of_graph_prop {α : Type u_1} {r : Relation α α} (h : r.comp r = r) (h' : r ∩ r.inv = Relation.diag) : IsPartialOrder r

instance opPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (Op α)

Equations

• opPartialOrder = PartialOrder.mk ⋯

instance instPartialOrderWithEq {α : Type u_1} : PartialOrder (WithEq α)

Equations

• instPartialOrderWithEq = PartialOrder.mk ⋯

instance instPartialOrderSet {α : Type u_1} : PartialOrder (Set α)

Equations

• instPartialOrderSet = PartialOrder.mk ⋯

@[simp]

theorem le_set_iff_subset {α : Type u_1} {a b : Set α} : a ≤ b ↔ a ⊆ b

instance instPartialOrderPartialMap {α : Type u_1} {β : α → Type u_2} : PartialOrder (PartialMap α β)

Equations

• instPartialOrderPartialMap = PartialOrder.mk ⋯

instance instPreorderCovering {α : Type u_1} : Preorder (Set.Covering α)

Equations

• instPreorderCovering = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderPartition {α : Type u_1} : PartialOrder (Set.Partition α)

Equations

• instPartialOrderPartition = PartialOrder.mk ⋯

instance instPartialOrderQuotEquiv {α : Type u_1} [Preorder α] : PartialOrder (Preorder.QuotEquiv α)

Equations

• instPartialOrderQuotEquiv = PartialOrder.mk ⋯

instance instPreorderPointwise {α : Type u_1} {β : α → Type u_2} [(x : α) → Preorder (β x)] : Preorder (Pointwise α β)

Equations

• instPreorderPointwise = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderPointwise {α : Type u_1} {β : α → Type u_2} [(x : α) → PartialOrder (β x)] : PartialOrder (Pointwise α β)

Equations

• instPartialOrderPointwise = PartialOrder.mk ⋯

theorem pointwise_graph_product {α : Type u_1} {β : α → Type u_2} [(x : α) → LE (β x)] : LE.le_rel = (fun (x : (i : α) → β i × β i) => (fun (a : α) => (x a).fst, fun (a : α) => (x a).snd)) '' Πˢ _i : α, LE.le_rel

@[simp]

theorem Preorder.quotEquiv_le_iff {α : Type u_1} [Preorder α] {a b : α} : Preorder.QuotEquiv.mk a ≤ Preorder.QuotEquiv.mk b ↔ a ≤ b

instance instPreorderProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Preorder (α × β)

Equations

• instPreorderProd = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderProd {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] : PartialOrder (α × β)

Equations

• instPartialOrderProd = PartialOrder.mk ⋯

def Comparable {α : Type u_1} [Preorder α] (x y : α) : Prop

Equations

• Comparable x y = (x ≤ y ∨ y ≤ x)

def Incomparable {α : Type u_1} [Preorder α] (x y : α) : Prop

Equations

• Incomparable x y = (¬x ≤ y ∧ ¬y ≤ x)

theorem incomparable_iff_not_comparable {α : Type u_1} [Preorder α] {x y : α} : Incomparable x y ↔ ¬Comparable x y

theorem not_incomparable_iff_comparable {α : Type u_1} [Preorder α] {x y : α} : Comparable x y ↔ ¬Incomparable x y