covariant_of_const — Mathlib

English

If f is monotone and μ m is a covariant operator, then the composition x ↦ f(μ m x) is monotone.

Русский

Если f монотонна и μ m — ковариантный оператор, тогда композиция x ↦ f(μ m x) монотонна.

LaTeX

$$$\text{If } Monotone(f) \text{ and } CovariantClass\, M N μ \le, \text{ then } Monotone(\lambda x\, f(μ(m,x)))$$$

Lean4

/-- A monotone function remains monotone when composed with the partial application
of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (m + n))`. -/
theorem covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Monotone f) (m : M) : Monotone (f <| μ m ·) :=
  hf.comp (Covariant.monotone_of_const m)

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