class RightDirected (α : Type u_2) [Preorder α] : Prop

• exists_ub : ∀ (x y : α), ∃ (a : α), x ≤ a ∧ y ≤ a

noncomputable def RightDirected.ub {α : Type u_1} [Preorder α] [RightDirected α] (x y : α) : α

Equations

• RightDirected.ub x y = ⋯.choose

class LeftDirected (α : Type u_2) [Preorder α] : Prop

• exists_lb : ∀ (x y : α), ∃ (a : α), a ≤ x ∧ a ≤ y

noncomputable def LeftDirected.lb {α : Type u_1} [Preorder α] [LeftDirected α] (x y : α) : α

Equations

• LeftDirected.lb x y = ⋯.choose

@[simp]

theorem RightDirected.ub_upperBound {α : Type u_1} [Preorder α] [RightDirected α] {x y : α} : UpperBound {x, y} (RightDirected.ub x y)

@[simp]

theorem LeftDirected.lb_lowerBound {α : Type u_1} [Preorder α] [LeftDirected α] {x y : α} : LowerBound {x, y} (LeftDirected.lb x y)

@[simp]

theorem RightDirected.le_ub_left {α : Type u_1} [Preorder α] [RightDirected α] {x y : α} : x ≤ RightDirected.ub x y

@[simp]

theorem RightDirected.le_ub_right {α : Type u_1} [Preorder α] [RightDirected α] {x y : α} : y ≤ RightDirected.ub x y

@[simp]

theorem LeftDirected.lb_le_left {α : Type u_1} [Preorder α] [LeftDirected α] {x y : α} : LeftDirected.lb x y ≤ x

@[simp]

theorem LeftDirected.lb_le_right {α : Type u_1} [Preorder α] [LeftDirected α] {x y : α} : LeftDirected.lb x y ≤ y

def Greatest.rightDirected {α : Type u_1} [Preorder α] {a : α} (h : Greatest a) : RightDirected α

Equations

• ⋯ = ⋯

def Least.leftDirected {α : Type u_1} [Preorder α] {a : α} (h : Least a) : LeftDirected α

Equations

• ⋯ = ⋯

theorem RightDirected.maximal_greatest {α : Type u_1} [PartialOrder α] [RightDirected α] {a : α} (h : Maximal a) : Greatest a

theorem LeftDirected.minimal_least {α : Type u_1} [PartialOrder α] [LeftDirected α] {a : α} (h : Minimal a) : Least a

theorem RightDirected.maximal_iff_greatest {α : Type u_1} [PartialOrder α] [RightDirected α] {a : α} : Maximal a ↔ Greatest a

theorem LeftDirected.minimal_iff_least {α : Type u_1} [PartialOrder α] [LeftDirected α] {a : α} : Minimal a ↔ Least a

theorem rightDirected_op_iff_leftDirected {α : Type u_1} [Preorder α] : RightDirected (Op α) ↔ LeftDirected α

theorem leftDirected_op_iff_rightDirected {α : Type u_1} [Preorder α] : LeftDirected (Op α) ↔ RightDirected α

instance instRightDirectedPointwise {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] [∀ (i : ι), RightDirected (α i)] : RightDirected (Pointwise ι α)

Equations

• ⋯ = ⋯

instance instLeftDirectedPointwise {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] [∀ (i : ι), LeftDirected (α i)] : LeftDirected (Pointwise ι α)

Equations

• ⋯ = ⋯

theorem RightDirected.cofinal_subset {α : Type u_1} [Preorder α] [RightDirected α] {s : Set α} (h : Cofinal s) : RightDirected ↥s

theorem LeftDirected.cofinal_subset {α : Type u_1} [Preorder α] [LeftDirected α] {s : Set α} (h : Coinitial s) : LeftDirected ↥s