instFunLikeAddContentSetENNReal — Mathlib

English

An additive content on a set family is modeled as a function-like object with values in ENNReal.

Русский

Аддитивная содержательность задаётся как объект, ведущий себя как функция, со значениями в ENNReal.

LaTeX

$$AddContent C is a structure with a function to Set α into ENNReal, i.e., a FunLike (Set α) ENNReal$$

Lean4

instance : FunLike (AddContent C) (Set α) ℝ≥0∞
    where
  coe m s := m.toFun s
  coe_injective' m m'
    _ := by
    cases m
    cases m'
    congr

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