le_min

Mathlib.Order.Defs.LinearOrder

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

English

If c ≤ a and c ≤ b then c ≤ min a b.

Русский

Если c ≤ a и c ≤ b, то c ≤ min(a,b).

LaTeX

$$$ (c \le a) \land (c \le b) \rightarrow c \le \min(a,b) $$$

Lean4

theorem le_min (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b := by grind

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

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

Разделы

Аффилиация

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