Mathlib.Order.Part

Monotone.partBind theorem

(hf : Monotone f) (hg : Monotone g) : Monotone fun x ↦ (f x).bind (g x)

Full source

lemma Monotone.partBind (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x ↦ (f x).bind (g x) := by
  rintro x y h a
  simp only [and_imp, exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Monotonicity of Partial Value Binding

Informal description

Let $f$ and $g$ be monotone functions. Then the function $x \mapsto \mathrm{bind}\,(f\,x)\,(g\,x)$ is also monotone, where $\mathrm{bind}$ is the partial value binding operation on `Part`.

Antitone.partBind theorem

(hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ (f x).bind (g x)

Full source

lemma Antitone.partBind (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x ↦ (f x).bind (g x) := by
  rintro x y h a
  simp only [and_imp, exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Antitonicity of Partial Value Binding under Antitone Functions

Informal description

Let $f$ and $g$ be antitone functions. Then the function $x \mapsto \mathrm{bind}\,(f\,x)\,(g\,x)$ is also antitone, where $\mathrm{bind}$ is the partial value binding operation on `Part`.

Monotone.partMap theorem

(hg : Monotone g) : Monotone fun x ↦ (g x).map f

Full source

lemma Monotone.partMap (hg : Monotone g) : Monotone fun x ↦ (g x).map f := by
  simpa only [← bind_some_eq_map] using hg.partBind monotone_const

Monotonicity of Partial Value Mapping under Monotone Functions

Informal description

Let $g$ be a monotone function. Then the function $x \mapsto \mathrm{map}\, f\,(g\,x)$ is also monotone, where $\mathrm{map}$ is the partial value mapping operation on `Part`.

Antitone.partMap theorem

(hg : Antitone g) : Antitone fun x ↦ (g x).map f

Full source

lemma Antitone.partMap (hg : Antitone g) : Antitone fun x ↦ (g x).map f := by
  simpa only [← bind_some_eq_map] using hg.partBind antitone_const

Antitonicity of Partial Value Mapping under Antitone Functions

Informal description

Let $g$ be an antitone function. Then the function $x \mapsto \mathrm{map}\, f\,(g\,x)$ is also antitone, where $\mathrm{map}$ is the partial value mapping operation on `Part`.

Monotone.partSeq theorem

(hf : Monotone f) (hg : Monotone g) : Monotone fun x ↦ f x <*> g x

Full source

lemma Monotone.partSeq (hf : Monotone f) (hg : Monotone g) : Monotone fun x ↦ f x <*> g x := by
  simpa only [seq_eq_bind_map] using hf.partBind <| Monotone.of_apply₂ fun _ ↦ hg.partMap

Monotonicity of Sequential Application on Partial Values

Informal description

Let $f$ and $g$ be monotone functions. Then the function $x \mapsto f\,x \mathbin{<*>} g\,x$ is also monotone, where $\mathbin{<*>}$ is the sequential application operation on `Part`.

Antitone.partSeq theorem

(hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ f x <*> g x

Full source

lemma Antitone.partSeq (hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ f x <*> g x := by
  simpa only [seq_eq_bind_map] using hf.partBind <| Antitone.of_apply₂ fun _ ↦ hg.partMap

Antitonicity of Sequential Application for Antitone Functions on Partial Values

Informal description

Let $f$ and $g$ be antitone functions. Then the function $x \mapsto f\,x \mathbin{<*>} g\,x$ is also antitone, where $\mathbin{<*>}$ is the sequential application operation on partial values.

OrderHom.partBind definition

(f : α →o Part β) (g : α →o β → Part γ) : α →o Part γ

Full source

/-- `Part.bind` as a monotone function -/
@[simps]
def partBind (f : α →o Part β) (g : α →o β → Part γ) : α →o Part γ where
  toFun x := (f x).bind (g x)
  monotone' := f.2.partBind g.2

Monotone partial binding of order homomorphisms

Informal description

Given two order homomorphisms $f : \alpha \to_o \text{Part} \beta$ and $g : \alpha \to_o (\beta \to \text{Part} \gamma)$, the function $\text{OrderHom.partBind} f g$ is defined as the order homomorphism from $\alpha$ to $\text{Part} \gamma$ where for each $x \in \alpha$, the value is given by the partial value binding $(f x).\text{bind} (g x)$. This operation is monotone with respect to the partial order on partial values.