const_mono — Mathlib

English

The map β ↦ (α → β → α) given by const β is monotone, i.e., for all a ≤ a' we have (const β) a ≤ (const β) a' in the pointwise order on functions β → α.

Русский

Отображение β ↦ (α → β → α), задаваемое константой β, монотонно: если a ≤ a', то (const β) a ≤ (const β) a' по точечно-упорядоченному отношению на функциях β → α.

LaTeX

$$$\forall a, a':\ a \le a' \Rightarrow (\mathrm{const}\ \beta\ a) \le (\mathrm{const}\ \beta\ a')$$$

Lean4

theorem const_mono : Monotone (const β : α → β → α) := fun _ _ h _ ↦ h

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