min_def_lt

Mathlib.Order.Basic

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

English

The minimum of a and b equals a if a < b, otherwise it equals b (i.e., min a b = if a < b then a else b).

Русский

Минимум(a,b) равен a, если a < b, иначе равен b.

LaTeX

$$$ \\min a b = \\begin{cases} a, & a < b \\\\ b, & \\text{иначе} \\end{cases} $$$

Lean4

theorem min_def_lt (a b : α) : min a b = if a < b then a else b := by rw [min_comm, min_def, ← ite_not];
  simp only [not_le]

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

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

Разделы

Аффилиация

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