lt_sub_iff_add_lt — Mathlib

English

Let a,b,c ∈ EReal with nondegenerate bounds. Then c < a - b ↔ c + b < a.

Русский

Пусть a,b,c ∈ EReal с невыраженными границами. Тогда c < a − b ↔ c + b < a.

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ (b \neq \bot \lor c \neq \top) \Rightarrow (b \neq \top \lor c \neq \bot) \\rightarrow (c < a - b \iff c + b < a)$$$

Lean4

protected theorem lt_sub_iff_add_lt {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : c < a - b ↔ c + b < a :=
  lt_iff_lt_of_le_iff_le (sub_le_iff_le_add h₁ h₂)

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