sub_eq_sInf — Mathlib

English

Let a, b be extended nonnegative reals. Then a − b equals the infimum of the set {d ∈ ℝ≥0∞ : a ≤ d + b}.

Русский

Пусть a, b ∈ ℝ≥0∞. Тогда a − b равно инфимуму множества {d ∈ ℝ≥0∞ : a ≤ d + b}.

LaTeX

$$$$ a - b = \operatorname{sInf}\{ d \in \mathbb{R}_{\ge 0}^{\infty} \mid a \le d + b \} $$$$

Lean4

theorem sub_eq_sInf {a b : ℝ≥0∞} : a - b = sInf {d | a ≤ d + b} :=
  le_antisymm (le_sInf fun _ h => tsub_le_iff_right.mpr h) <| sInf_le <| mem_setOf.2 le_tsub_add

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