monotone_of_const — Mathlib

English

For each m ∈ M, the map x ↦ μ(m,x) is monotone.

Русский

Для каждого m ∈ M отображение x ↦ μ(m,x) монотонно по отношению к порядку.

LaTeX

$$$\forall m\in M\;\Monotone(\lambda x\,\,\, μ(m,x))$$$

Lean4

/-- The partial application of a constant to a covariant operator is monotone. -/
theorem monotone_of_const [CovariantClass M N μ (· ≤ ·)] (m : M) : Monotone (μ m) := fun _ _ ↦ CovariantClass.elim m

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