English
A comparison in EReal can be characterized by the signs of the operands and their absolute values; x ≤ y iff the given sign-case condition holds.
Русский
Сравнение в EReal может быть охарактеризовано по знакам и модулю; x ≤ y тогда и только тогда, когда выполняется указанное разветвление по знакам.
LaTeX
$$$ x \le y \iff \begin{aligned} & \text{sign}(x) < \text{sign}(y) \ \lor\ \\ & (\text{sign}(x) = \text{neg} \wedge \text{sign}(y) = \text{neg} \wedge y.abs \le x.abs) \lor\ \\ & (\text{sign}(x) = \text{zero} \wedge \text{sign}(y) = \text{zero}) \lor\ \\ & (\text{sign}(x) = \text{pos} \wedge \text{sign}(y) = \text{pos} \wedge x.abs \le y.abs) \end{aligned} $$$
Lean4
theorem le_iff_sign {x y : EReal} :
x ≤ y ↔
sign x < sign y ∨
sign x = SignType.neg ∧ sign y = SignType.neg ∧ y.abs ≤ x.abs ∨
sign x = SignType.zero ∧ sign y = SignType.zero ∨
sign x = SignType.pos ∧ sign y = SignType.pos ∧ x.abs ≤ y.abs :=
by
constructor
· intro h
refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
cases hy : sign y <;> rw [hs, hy] at h ⊢
· simp
· left; simpa using h
· right; right; simpa using h
· rintro (h | h | h | h)
· exact (sign.monotone.reflect_lt h).le
all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]
