canLift — Mathlib

English

There is a CanLift instance allowing lifting from Real to NNReal given a nonneg predicate.

Русский

Существует экземпляр CanLift, позволяющий поднимать из Real в NNReal при выполнении неотрицательного условия.

LaTeX

$$$ \\text{CanLift}(\\mathbb{R}, \\mathbb{R}_{\\ge 0}, \\mathrm{toReal}, \\lambda r . 0 \\le r) $$$

Lean4

instance canLift : CanLift ℝ ℝ≥0 toReal fun r => 0 ≤ r :=
  Subtype.canLift _

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