max_cases — Mathlib

English

For any a,b in a linear order, max(a,b) = a and b ≤ a, or max(a,b) = b and a < b.

Русский

Для любых a,b в линейном порядке max(a,b) = a и b ≤ a, или max(a,b) = b и a < b.

LaTeX

$$$$\max(a,b) = a \land b \le a \;\,\lor\;\max(a,b) = b \land a < b.$$$$

Lean4

/-- For elements `a` and `b` of a linear order, either `max a b = a` and `b ≤ a`,
or `max a b = b` and `a < b`.
Use cases on this lemma to automate linarith in inequalities -/
theorem max_cases (a b : α) : max a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b :=
  @min_cases αᵒᵈ _ a b

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