instFunLikeCompactsENNReal — Mathlib

English

There exists a canonical FunLike structure making the type Content G act as a FunLike from the type of Content G to the type of ENNReal on the compact sets of G.

Русский

Существует каноническая структура FunLike, делающая Content G объектом FunLike между Content G и ENNReal на множествах компактов G.

LaTeX

$$$$ \\text{Content } G \\ \\text{has a canonical } \\text{FunLike } (\\text{Compacts } G) \\ ENNReal. $$$$

Lean4

instance : FunLike (Content G) (Compacts G) ℝ≥0∞
    where
  coe μ s := μ.toFun s
  coe_injective' := by rintro ⟨μ, _, _⟩ ⟨v, _, _⟩ h; congr!; ext s : 1; exact ENNReal.coe_injective <| congr_fun h s

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