max_eq_iff

Mathlib.Order.MinMax

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

English

max(a,b) = c iff (a = c and b ≤ a) or (b = c and a ≤ b).

Русский

max(a,b) = c тогда и только тогда, когда (a = c и b ≤ a) или (b = c и a ≤ b).

LaTeX

$$$$\max(a,b) = c \iff (a = c \land b \le a) \lor (b = c \land a \le b).$$$$

Lean4

theorem max_eq_iff : max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b :=
  @min_eq_iff αᵒᵈ _ a b c

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

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

Разделы

Аффилиация

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