min_one

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

English

Similarly, min(a, 1) = 1 whenever 1 ≤ a in a canonically ordered monoid.

Русский

Аналогично, min(a, 1) = 1 при 1 ≤ a в канонически упорядоченном моноиде.

LaTeX

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

Lean4

@[to_additive]
theorem min_one (a : α) : min a 1 = 1 :=
  min_eq_right (one_le a)

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

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

Разделы

Аффилиация

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