theorem
Finset.sum_image_le_of_nonneg
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[DecidableEq α]
[OrderedAddCommMonoid β]
[SMulPosMono ℕ β]
{J : Finset ι}
{g : ι → α}
{f : α → β}
(hf : ∀ u ∈ Finset.image g J, 0 ≤ f u)
:
∑ u ∈ Finset.image g J, f u ≤ ∑ u ∈ J, f (g u)
theorem
Finset.sum_image_of_disjoint
{ι : Type u_3}
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[OrderBot α]
[DecidableEq α]
[AddCommMonoid β]
{g : α → β}
(hg_bot : g ⊥ = 0)
{f : ι → α}
{I : Finset ι}
(hf_disj : (↑I).PairwiseDisjoint f)
:
∑ s ∈ Finset.image f I, g s = ∑ i ∈ I, g (f i)
theorem
Finset.prod_image_of_disjoint
{ι : Type u_3}
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[OrderBot α]
[DecidableEq α]
[CommMonoid β]
{g : α → β}
(hg_bot : g ⊥ = 1)
{f : ι → α}
{I : Finset ι}
(hf_disj : (↑I).PairwiseDisjoint f)
:
∏ s ∈ Finset.image f I, g s = ∏ i ∈ I, g (f i)
theorem
MeasurableSet.accumulate
{α : Type u_1}
:
∀ {x : MeasurableSpace α} {s : ℕ → Set α},
(∀ (n : ℕ), MeasurableSet (s n)) → ∀ (n : ℕ), MeasurableSet (Set.Accumulate s n)
theorem
Set.accumulate_succ
{α : Type u_1}
(s : ℕ → Set α)
(n : ℕ)
:
Set.Accumulate s (n + 1) = Set.Accumulate s n ∪ s (n + 1)