partSeq — Mathlib

English

If f: α → Part(β → γ) is monotone and g: α → Part β is monotone, then the pointwise application x ↦ f(x) <*> g(x) is monotone.

Русский

Пусть f: α → Part(β → γ) монотонна и g: α → Part β монотонна; тогда поэлементное применение x ↦ f(x) <*> g(x) также монотонно.

LaTeX

$$$\\mathrm{Monotone}(f) \\wedge \\mathrm{Monotone}(g) \\Rightarrow \\mathrm{Monotone}\\big( x \\mapsto f(x) \\;<*>\\; g(x) \\big)$$$

Lean4

theorem 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

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