one_mono

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#Pi.one_mono

English

The constant-1 map 1: α → β is monotone when β is equipped with an order and α is arbitrary (with β having a One and a preorder).

Русский

Пусть β имеет порядок и единицу, тогда константная карта 1: α → β монотонеальна.

LaTeX

$$$ \text{Monotone}(1 : \alpha \to \beta) $$$

Lean4

@[to_additive]
theorem one_mono [One β] : Monotone (1 : α → β) :=
  monotone_const

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru