Lean4
/-- A summable family can be reindexed by an embedding without changing its sum. -/
def embDomain (s : SummableFamily Γ R α) (f : α ↪ β) : SummableFamily Γ R β
where
toFun b := if h : b ∈ Set.range f then s (Classical.choose h) else 0
isPWO_iUnion_support' :=
by
refine s.isPWO_iUnion_support.mono (Set.iUnion_subset fun b g h => ?_)
by_cases hb : b ∈ Set.range f
· rw [dif_pos hb] at h
exact Set.mem_iUnion.2 ⟨Classical.choose hb, h⟩
· simp [-Set.mem_range, dif_neg hb] at h
finite_co_support'
g :=
((s.finite_co_support g).image f).subset
(by
intro b h
by_cases hb : b ∈ Set.range f
· simp only [Ne, Set.mem_setOf_eq, dif_pos hb] at h
exact ⟨Classical.choose hb, h, Classical.choose_spec hb⟩
· simp only [Ne, Set.mem_setOf_eq, dif_neg hb, coeff_zero, not_true_eq_false] at h)
