English
If f and g are analytic in their respective groupoids I and J, then their product f.prod g is analytic in the product groupoid I.prod J.
Русский
Если f и g аналитичны в соответствующих группоидах I и J, то их произведение f.prod g аналитично в группоиde I.prod J.
LaTeX
$$$f \in analyticGroupoid(I) \land g \in analyticGroupoid(J) \Rightarrow f \! .prod\! g \in analyticGroupoid(I \prod J)$$$
Lean4
/-- `analyticGroupoid` is closed under products -/
theorem analyticGroupoid_prod {E A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace A] {F B : Type}
[NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] {I : ModelWithCorners 𝕜 E A}
{J : ModelWithCorners 𝕜 F B} {f : OpenPartialHomeomorph A A} {g : OpenPartialHomeomorph B B}
(fa : f ∈ analyticGroupoid I) (ga : g ∈ analyticGroupoid J) : f.prod g ∈ analyticGroupoid (I.prod J) :=
by
have pe : range (I.prod J) = (range I).prod (range J) := I.range_prod
simp only [mem_analyticGroupoid] at fa ga ⊢
exact
⟨AnalyticOn.prod (fa.1.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
(ga.1.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩),
AnalyticOn.prod (fa.2.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
(ga.2.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩
