English
Let f: α →o Part β and g: α →o β → Part γ be order-preserving. Then x ↦ (f x).bind (g x) is order-preserving from α to Part γ.
Русский
Пусть f: α →o Part β и g: α →o β → Part γ — монотонны; тогда x ↦ (f x).bind (g x) является монотонной по x функцией от α в Part γ.
LaTeX
$$$\\text{OrderPreserving}(f) \\land \\text{OrderPreserving}(g) \\Rightarrow \\text{OrderPreserving}\\big( x \\mapsto (f(x)).bind (g(x)) \\big)$$$
Lean4
/-- `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
