lt_add_iff — Mathlib

English

If c ≠ 0, then a < b + c iff exists d < c with a ≤ b + d.

Русский

Если c ≠ 0, то a < b + c тогда и только если найдется d < c такое, что a ≤ b + d.

LaTeX

$$(c \neq 0) \Rightarrow \left(a < b + c \iff \exists d < c, a \le b + d\right)$$

Lean4

theorem lt_add_iff {a b c : Ordinal} (hc : c ≠ 0) : a < b + c ↔ ∃ d < c, a ≤ b + d :=
  by
  use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩
  rintro ⟨d, hd, ha⟩
  exact ha.trans_lt (add_lt_add_left hd b)

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