def Op (α : Type u_1) : Type u_1

put opposite relation etc on a type

Equations

• Op α = α

def toOp {α : Type u_1} (x : α) : Op α

Equations

• toOp x = x

def fromOp {α : Type u_1} (x : Op α) : α

Equations

• fromOp x = x

theorem toOp_fromOp {α : Type u_1} {x : Op α} : toOp (fromOp x) = x

theorem fromOp_toOp {α : Type u_1} {x : α} : fromOp (toOp x) = x

instance opLE {α : Type u_1} [LE α] : LE (Op α)

Equations

• opLE = { le := fun (x y : Op α) => y ≤ x }

instance opLT {α : Type u_1} [LT α] : LT (Op α)

Equations

• opLT = { lt := fun (x y : Op α) => y < x }

@[simp]

theorem toOp_le_iff {α : Type u_1} [LE α] {x y : α} : toOp x ≤ toOp y ↔ y ≤ x

@[simp]

theorem fromOp_le_iff {α : Type u_1} [LE α] {x y : Op α} : fromOp x ≤ fromOp y ↔ y ≤ x

@[simp]

theorem toOp_lt_iff {α : Type u_1} [LT α] {x y : α} : toOp x < toOp y ↔ y < x

@[simp]

theorem fromOp_lt_iff {α : Type u_1} [LT α] {x y : Op α} : fromOp x < fromOp y ↔ y < x

structure PartialMap (α : Type u_2) (β : α → Type u_3) : Type (max u_2 u_3)

extension order for functions

• carrier : Set α
• function : (x : ↥self.carrier) → β x.val

instance piExtendsLE {α : Type u_2} {β : α → Type u_3} : LE (PartialMap α β)

Equations

• piExtendsLE = { le := fun (x y : PartialMap α β) => ∃ (h : x.carrier ⊆ y.carrier), ∀ (a : α) (h' : a ∈ x.carrier), y.function ⟨a, ⋯⟩ = x.function ⟨a, h'⟩ }

def RelAsLE {α : Type u_2} : Relation α α → Type u_2

Equations

• RelAsLE x = α

instance instLERelAsLE {α : Type u_2} {r : Relation α α} : LE (RelAsLE r)

Equations

• instLERelAsLE = { le := fun (x y : RelAsLE r) => (x, y) ∈ r }

def RelAsLT {α : Type u_2} : Relation α α → Type u_2

Equations

• RelAsLT x = α

instance instLTRelAsLT {α : Type u_2} {r : Relation α α} : LT (RelAsLT r)

Equations

• instLTRelAsLT = { lt := fun (x y : RelAsLT r) => (x, y) ∈ r }

def Pointwise (α : Type u_4) (β : α → Type u_5) : Type (max u_4 u_5)

Equations

• Pointwise α β = ((x : α) → β x)

instance instLEPointwise {α : Type u_2} {β : α → Type u_3} [(x : α) → LE (β x)] : LE (Pointwise α β)

Equations

• instLEPointwise = { le := fun (f g : Pointwise α β) => ∀ (x : α), f x ≤ g x }