const_strictMono — Mathlib

English

If β is nonempty, then the map const β : α → β → α is strictly monotone, i.e., a < a' implies (const β) a < (const β) a' (in the pointwise order).

Русский

Если β непуста, то константное отображение константной функции является строго монотонным: a < a' ⇒ (const β) a < (const β) a' (по точечному порядку).

LaTeX

$$$[\text{Nonempty } \beta] \Rightarrow (\forall a\,a',\ a < a' \Rightarrow (\mathrm{const}\ \beta\ a) < (\mathrm{const}\ \beta\ a'))$$$

Lean4

theorem const_strictMono [Nonempty β] : StrictMono (const β : α → β → α) := fun _ _ ↦ const_lt_const.2

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