English
If maps φ_j between factors are continuous and satisfy compatibility, then the induced map mapAlong is continuous.
Русский
Если каждое сопоставление φ_j непрерывно и совместимо, то полученная карта mapAlong непрерывна.
LaTeX
$$$\\mathrm{Continuous}\\big(\\mathrm{RestrictedProduct}.\\mathrm{mapAlong}(\\cdot)\\big)$$$
Lean4
theorem mapAlong_continuous (φ_cont : ∀ j, Continuous (φ j)) : Continuous (mapAlong R₁ R₂ f hf φ hφ) :=
by
rw [continuous_dom]
intro S hS
set T := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
have hT : 𝓕₂ ≤ 𝓟 T := by
rw [le_principal_iff] at hS ⊢
exact inter_mem (hf hS) hφ
have hf' : Tendsto f (𝓟 T) (𝓟 S) := by aesop
have hφ' : ∀ᶠ j in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j) := by aesop
have key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS = inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ' := rfl
rw [key]
exact
continuous_inclusion _ |>.comp <|
continuous_rng_of_principal.mpr <| continuous_pi fun j ↦ φ_cont j |>.comp <| continuous_eval (f j)
