coe_mk — Mathlib

English

There is a natural scalar action of C(α, γ) on the subtype of compactly supported bounded continuous functions, sending a pair (g, f) to the product gf with HasCompactSupport.

Русский

Существует естественное скалярное действие C(α, γ) на подтипе компактно поддерживаемых ограниченно непрерывных функций, отправляющее пару (g, f) в произведение gf с HasCompactSupport.

LaTeX

$$HasCompactSupport (instHMul.hMul (ContinuousMap.instFunLike.coe g) (BoundedContinuousFunction.instFunLike.coe f.val))$$

Lean4

@[simp]
theorem coe_mk (f : C(α, β)) (h : Tendsto f (cocompact α) (cocompact β)) : ⇑(⟨f, h⟩ : CocompactMap α β) = f :=
  rfl

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