English
Equivalences of the parametrizing type extend to summable families; they preserve the summable structure via the Equiv construction.
Русский
Эквиваленции параметрирующего множества распространяются на суммируемые семейства, сохраняя структуру суммируемости через конструкцию Equiv.
LaTeX
$$$\\text{Equiv}(e,s):\\;\\text{SummableFamily } Γ R α \\to \\text{SummableFamily } Γ R β$ with toFun(b)=s(e^{-1}(b))$$
Lean4
/-- A summable family induced by an equivalence of the parametrizing type. -/
@[simps]
def Equiv (e : α ≃ β) (s : SummableFamily Γ R α) : SummableFamily Γ R β
where
toFun b := s (e.symm b)
isPWO_iUnion_support' := by
refine Set.IsPWO.mono s.isPWO_iUnion_support fun g => ?_
simp only [Set.mem_iUnion, mem_support, ne_eq, forall_exists_index]
exact fun b hg => Exists.intro (e.symm b) hg
finite_co_support' g := (Equiv.set_finite_iff e.subtypeEquivOfSubtype').mp <| s.finite_co_support' g
