canLift — Mathlib

English

There is a lifting instance that allows lifting a continuous map from C(X, R) to C(X, R≥0) when the map is nonnegative pointwise.

Русский

Существуют условия подъёма, позволяющие перейти от непрерывного отображения в R к в R≥0 по точкам неотрицательных значений.

LaTeX

$$$\\text{CanLift } C(X, \\mathbb{R}) C(X, \\mathbb{R}_{\\ge 0}) \\text{ContinuousMap.coeNNRealReal} \\big( \\text{pointwise nonnegativity} \\big)$$$

Lean4

instance canLift {X : Type*} [TopologicalSpace X] :
    CanLift C(X, ℝ) C(X, ℝ≥0) ContinuousMap.coeNNRealReal.comp fun f => ∀ x, 0 ≤ f x where
  prf f hf := ⟨⟨fun x => ⟨f x, hf x⟩, f.2.subtype_mk _⟩, DFunLike.ext' rfl⟩

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