sub_nonneg — Mathlib

English

If not both top and not both bottom hold, then 0 ≤ x − y iff y ≤ x.

Русский

При условии, что не выполняются обе top и не выполняются обе bottom, верно 0 ≤ x − y ⇔ y ≤ x.

LaTeX

$$$$\bigl( x \neq \top \lor y \neq \top \bigr) \land \bigl( x \neq \bot \lor y \neq \bot \bigr) \Rightarrow \bigl(0 \le x - y \iff y \le x\bigr).$$$$

Lean4

theorem sub_nonneg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x := by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

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