English
If p ≤ q in ENNReal, then one of several exhaustive cases holds: (p = 0, q = 0); (p = 0, q = ∞); (p = 0, 0 < q.toReal); (p = ∞, q = ∞); (0 < p.toReal, q = ∞); or (0 < p.toReal, 0 < q.toReal, p.toReal ≤ q.toReal).
Русский
Если p ≤ q в ENNReal, то выполняется одно из перечисленных взаимоисключающих условий: (p=0, q=0); (p=0, q=∞); (p=0, 0<q.toReal); (p=∞, q=∞); (0<p.toReal, q=∞); или (0<p.toReal, 0<q.toReal, p.toReal ≤ q.toReal).
LaTeX
$$$p \le q \Rightarrow (p = 0 \land q = 0) \lor (p = 0 \land q = \infty) \lor (p = 0 \land 0 < q.toReal) \lor (p = \infty \land q = \infty) \lor (0 < p.toReal \land q = \infty) \lor (0 < p.toReal \land 0 < q.toReal \land p.toReal \le q.toReal)$$$
Lean4
protected theorem trichotomy₂ {p q : ℝ≥0∞} (hpq : p ≤ q) :
p = 0 ∧ q = 0 ∨
p = 0 ∧ q = ∞ ∨
p = 0 ∧ 0 < q.toReal ∨
p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal :=
by
rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
· simpa using q.trichotomy
rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
· simpa using p.trichotomy
have hq' : 0 < q := lt_of_lt_of_le hp hpq
have hp' : p < ∞ := lt_of_le_of_lt hpq hq
simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]
