English
An additive content on a semiring C can be extended to the same semiring by assigning the value ∞ to every set not in C, while keeping the value on sets in C unchanged. The extension preserves the empty set and sUnion in the appropriate sense.
Русский
Аддитивное содержимое на полусистеме C можно продолжить на ту же полусистему, задав для каждого множества вне C значение ∞ и сохранив значения на множествах внутри C.
LaTeX
$$$\tilde{m}(S) = \begin{cases} m(S), & S \in C, \\ \infty, & S \notin C. \end{cases}$$$
Lean4
/-- An additive content obtained from another one on the same semiring of sets by setting the value
of each set not in the semiring at `∞`. -/
protected noncomputable def extend (hC : IsSetSemiring C) (m : AddContent C) : AddContent C
where
toFun := extend (fun x (_ : x ∈ C) ↦ m x)
empty' := by rw [extend_eq, addContent_empty]; exact hC.empty_mem
sUnion' I h_ss h_dis
h_mem := by
rw [extend_eq]
swap; · exact h_mem
rw [addContent_sUnion h_ss h_dis h_mem]
refine Finset.sum_congr rfl (fun s hs ↦ ?_)
rw [extend_eq]
exact h_ss hs
