min_lt_min

Mathlib.Order.MinMax

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

English

min(a,b) < min(c,d) whenever a < c and b < d.

Русский

min(a,b) < min(c,d) при a < c и b < d.

LaTeX

$$$$ (a < c) \land (b < d) \Rightarrow \min(a,b) < \min(c,d). $$$$

Lean4

theorem min_lt_min (h₁ : a < c) (h₂ : b < d) : min a b < min c d :=
  @max_lt_max αᵒᵈ _ _ _ _ _ h₁ h₂

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

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

Разделы

Аффилиация

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