instNNRatCast — Mathlib

English

There is a canonical casting from nonnegative NN rational numbers into the nonnegative subtype.

Русский

Существует каноническое приведение неотрицательных рациональных чисел к неотрицательному подтипу.

LaTeX

$$$\\text{instNNRatCast} : NNRat \\to { x : α // 0 ≤ x }$ with $q \\mapsto ⟨q, q.cast\\_nonneg\\rangle$$$

Lean4

instance instNNRatCast : NNRatCast { x : α // 0 ≤ x } :=
  ⟨fun q ↦ ⟨q, q.cast_nonneg⟩⟩

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