Documentation

Mathlib.Order.Part

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} {γ : Type u_4} {f : αPart (βγ)} {g : αPart β} (hf : Monotone f) (hg : Monotone g) :
Monotone fun (x : α) => Seq.seq (f x) fun (x_1 : Unit) => g x
theorem Antitone.partSeq {α : Type u_1} [Preorder α] {β : Type u_4} {γ : Type u_4} {f : αPart (βγ)} {g : αPart β} (hf : Antitone f) (hg : Antitone g) :
Antitone fun (x : α) => Seq.seq (f x) fun (x_1 : Unit) => g x
@[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)
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' := }
Instances For
    @[deprecated OrderHom.partBind]
    def OrderHom.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] (f : α →o Part β) (g : α →o βPart γ) :
    α →o Part γ

    Alias of OrderHom.partBind.


    Part.bind as a monotone function

    Equations
    Instances For