realContinuousMapOfNNReal_apply_comp_toReal

English

A compatibility lemma: applying the real-continuous map after composing with toNNReal matches the direct application after the Real extension.

Русский

Лемма совместимости: применение realContinuousMapOfNNReal после композиции с toNNReal даёт тот же результат, что и прямое применение после расширения на Real.

LaTeX

$$Eq (φ.realContinuousMapOfNNReal (mk toReal ∘ coe).circ f) (φ f)$$

Lean4

@[simp high]
theorem realContinuousMapOfNNReal_apply_comp_toReal (φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A) (f : C(X, ℝ≥0)) :
    φ.realContinuousMapOfNNReal ((ContinuousMap.mk toReal continuous_coe).comp f) = φ f :=
  by
  simp only [realContinuousMapOfNNReal_apply]
  convert_to φ f - φ 0 = φ f using 2
  on_goal -1 => rw [map_zero, sub_zero]
  all_goals
    congr
    ext x
    simp

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