sub_lt_sub_of_lt_of_le — Mathlib

English

If x < y and z ≤ t with z ≠ ⊥ and t ≠ ⊤, then x − t < y − z.

Русский

Если x < y и z ≤ t с z ≠ ⊥ и t ≠ ⊤, то x − t < y − z.

LaTeX

$$$$x < y \Rightarrow z \le t \Rightarrow z \neq \bot \Rightarrow t \neq \top \Rightarrow x - t < y - z.$$$$

Lean4

theorem sub_lt_sub_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) : x - t < y - z :=
  add_lt_add_of_lt_of_le h (neg_le_neg_iff.2 h') (by simp [ht]) (by simp [hz])

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