const_le_one_of_le_one

Mathlib.Algebra.Order.Pi

URI: https://scilib.ai/kg/mathlib#Function.const_le_one_of_le_one

English

If a ≤ 1, then const β a ≤ 1.

Русский

Если a ≤ 1, то константная функция β → a ≤ 1.

LaTeX

$$$\\forall a,\\ (a \\le 1) \\Rightarrow (\\mathrm{const}_\\beta a \\le 1).$$$

Lean4

@[to_additive]
theorem const_le_one_of_le_one (ha : a ≤ 1) : const β a ≤ 1 := fun _ => ha

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

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

Разделы

Аффилиация

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