one_min

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

For a, the minimum of a and 1 equals 1, provided a ≥ 1 in a canonically ordered monoid.

Русский

Для a минимум между a и 1 равен 1, при условии a ≥ 1 в канонически упорядоченном моноиде.

LaTeX

$$min(1, a) = 1$$

Lean4

@[to_additive]
theorem one_min (a : α) : min 1 a = 1 :=
  min_eq_left (one_le a)

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

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

Разделы

Аффилиация

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