namespace  http://mathhub.info/MitM/core/typedsets ❚

import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
import ar http://mathhub.info/MitM/core/arithmetics ❚

theory SetSum : base:?Logic =
	include ☞ar:?RealArithmetics ❙
	include ☞ts:?FiniteSets ❙

	
	setSum : {A : type  , s : set ℝ} ⊦ s finite ⟶ (A ⟶ ℝ) ⟶ ℝ ❘# setSum 2 3 4 ❙
	setSum_empty : {A : type , f : A ⟶ ℝ} ⊦ setSum ∅ theorem_emptySetIsFinite f ≐ (0 : ℝ) ❙
	
	setSum_cons : {A : type , s : set ℝ ,  a : ℝ, p : ⊦ (s <- a) finite , f : A ⟶ ℝ} 
	⊦ setSum (s <- a) p f ≐ a + setSum s (theorem_setConsFiniteSplit ℝ s a p) f ❙
❚