monovary_const_right

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#monovary_const_right

English

Let f: ι → α and b ∈ β. Then the pair (f, const ι b) is Monovary.

Русский

Пусть f: ι → α и b ∈ β. Тогда пара функций (f, константная функция ι → β, значение b) образует моновариацию.

LaTeX

$$$\\operatorname{Monovary}(f, \\operatorname{const}_{\\iota} b)$$$

Lean4

theorem monovary_const_right (f : ι → α) (b : β) : Monovary f (const ι b) := fun _ _ h => (h.ne rfl).elim

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

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

Разделы

Аффилиация

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