Monotonicity of monadic operations on Part

theorem Monotone.partBind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → Part β} {g : α → β → Part γ} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : α) => (f x).bind (g x)

theorem Antitone.partBind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → Part β} {g : α → β → Part γ} (hf : Antitone f) (hg : Antitone g) : Antitone fun (x : α) => (f x).bind (g x)

theorem Monotone.partMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : β → γ} {g : α → Part β} (hg : Monotone g) : Monotone fun (x : α) => Part.map f (g x)

theorem Antitone.partMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : β → γ} {g : α → Part β} (hg : Antitone g) : Antitone fun (x : α) => Part.map f (g x)

theorem Monotone.partSeq {α : Type u_1} [Preorder α] {β γ : Type u_4} {f : α → Part (β → γ)} {g : α → Part β} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : α) => f x <*> g x

theorem Antitone.partSeq {α : Type u_1} [Preorder α] {β γ : Type u_4} {f : α → Part (β → γ)} {g : α → Part β} (hf : Antitone f) (hg : Antitone g) : Antitone fun (x : α) => f x <*> g x

def OrderHom.partBind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] (f : α →o Part β) (g : α →o β → Part γ) : α →o Part γ

Part.bind as a monotone function

Equations

• f.partBind g = { toFun := fun (x : α) => (f x).bind (g x), monotone' := ⋯ }

@[simp]

theorem OrderHom.partBind_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] (f : α →o Part β) (g : α →o β → Part γ) (x : α) : (f.partBind g) x = (f x).bind (g x)