English
For any a,b in a linear order, min(a,b) = a and a ≤ b, or min(a,b) = b and b < a.
Русский
Для любых a,b в линейном порядке min(a,b) = a и a ≤ b, или min(a,b) = b и b < a.
LaTeX
$$$$\min(a,b) = a \land a \le b \;\,\lor\;\min(a,b) = b \land b < a.$$$$
Lean4
/-- For elements `a` and `b` of a linear order, either `min a b = a` and `a ≤ b`,
or `min a b = b` and `b < a`.
Use cases on this lemma to automate linarith in inequalities -/
theorem min_cases (a b : α) : min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a :=
by
by_cases h : a ≤ b
· left
exact ⟨min_eq_left h, h⟩
· right
exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩
