instInhabitedContent — Mathlib

English

There is a FunLike structure on Content G with values in ENNReal, using coe μ s := μ.toFun s.

Русский

Существует структура FunLike на Content G со значениями в ENNReal, задаваемая коe μ s := μ.toFun s.

LaTeX

$$instFunLikeCompactsENNReal : FunLike (Content G) (Compacts G) ENNReal$$

Lean4

instance : Inhabited (Content G) :=
  ⟨{  toFun := fun _ => 0
      mono' := by simp
      sup_disjoint' := by simp
      sup_le' := by simp }⟩

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