partBind — Mathlib

English

If f : α → Part β and g : α → β → Part γ are monotone, then x ↦ (f x).bind (g x) is monotone.

Русский

Если f : α → Part β и g : α → β → Part γ монотонны, то x ↦ (f x).bind (g x) монотонна.

LaTeX

$$$$ \\text{Monotone } f \\to \\text{Monotone } g \\to \\text{Monotone }(x \\mapsto (f x).bind (g x)). $$$$

Lean4

theorem 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, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Похожие утверждения