sub_def — Mathlib

English

For r,p ∈ ℝ≥0, subtraction in NNReal agrees with real subtraction followed by embedding: r − p = Real.toNNReal (r − p).

Русский

Для r,p ∈ ℝ≥0 вычитание в NNReal согласуется с вещественным вычитанием, затем включением: r − p = Real.toNNReal (r − p).

LaTeX

$$$\forall r,p \in \mathbb{R}_{\ge 0},\ r - p = \text{Real.toNNReal}(r - p)$$$

Lean4

theorem sub_def {r p : ℝ≥0} : r - p = Real.toNNReal (r - p) :=
  rfl

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