covariant_of_const' — Mathlib

English

Same as Covariant Composition but with the constant on the other side, i.e., x ↦ f(μ(x,m)).

Русский

Аналогично предыдущему, но константа слева: x ↦ f(μ(x,m)).

LaTeX

$$$\text{Monotone}(\lambda x\, f(μ( x, m)))$ given Covariant with swap μ.$$

Lean4

/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
the operator.  E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (n + m))`. -/
theorem covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)] (hf : Monotone f) (m : N) :
    Monotone (f <| μ · m) :=
  Monotone.covariant_of_const (μ := swap μ) hf m

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