min_le_iff

Mathlib.Order.MinMax

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

English

In a linear order, min-quantities satisfy: min a b ≤ c iff a ≤ c or b ≤ c.

Русский

В линейном порядке минимумы удовлетворяют: min(a,b) ≤ c ⇔ a ≤ c или b ≤ c.

LaTeX

$$$\min(a,b) \le c \iff (a \le c \lor b \le c)$$$

Lean4

theorem min_le_iff : min a b ≤ c ↔ a ≤ c ∨ b ≤ c :=
  inf_le_iff

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

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

Разделы

Аффилиация

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