English
Let α, β, γ be types with a preorder on α. If g: α → Part β is monotone and f: β → γ is a function, then the map x ↦ (g(x)).map f is monotone.
Русский
Пусть α, β, γ — множества с предельной упорядоченностью, причём α обладает предельной структурой. Если g: α → Part β монотонна и f: β → γ, то отображение x ↦ (g(x)).map f монотонно по x.
LaTeX
$$$\\mathrm{Monotone}(g) \\Rightarrow \\mathrm{Monotone}\\big( x \\mapsto \\mathrm{Part.map}\\, f\\, (g\\,x) \\big)$$$
Lean4
theorem partMap (hg : Monotone g) : Monotone fun x ↦ (g x).map f := by
simpa only [← bind_some_eq_map] using hg.partBind monotone_const
