Analytic regrouping of finite families #
The regrouping homeomorphisms from TauCeti.Topology.PiCurry are coordinate projections and
finite products, so they and their inverses are analytic. These facts are kept here, beside the
homeomorphisms, so applications can reuse them without importing a root or polynomial development.
theorem
TauCeti.analyticAt_piSigmaConstHomeomorph
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
[Fintype ι]
{m : ι → ℕ}
{n : ℕ}
(e : (i : ι) × Fin (m i) ≃ Fin n)
(c : (i : ι) → Fin (m i) → 𝕜)
:
AnalyticAt 𝕜 (⇑(piSigmaConstHomeomorph 𝕜 e)) c
Regrouping a finite family of tuples is analytic.
theorem
TauCeti.analyticAt_piSigmaConstHomeomorph_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
[Fintype ι]
{m : ι → ℕ}
{n : ℕ}
(e : (i : ι) × Fin (m i) ≃ Fin n)
(c : Fin n → 𝕜)
:
AnalyticAt 𝕜 (⇑(piSigmaConstHomeomorph 𝕜 e).symm) c
The inverse regrouping from one tuple to a finite family of tuples is analytic.