English
A universal property with parameters: a map on a product with a Y-parameter space is continuous iff its restricted maps are continuous on each principal cross-section.
Русский
Универсальная свойство для произведений с параметрами: отображение непрерывно тогда и только тогда, когда его ограничения на каждую координатную секцию непрерывны.
LaTeX
$$$\\text{Continuous f} \\iff \\forall S, hS, \\ \\text{Continuous}(f \\circ (\\text{Prod.map} (\\text{inclusion } R A hS) \\tfrac{id}{}}$$$
Lean4
/-- The **universal property with parameters** of the topology on the restricted product:
for any topological space `Y` of "parameters", a map from `(Πʳ i, [R i, A i]) × Y` is continuous
*iff* its restriction to each `(Πʳ i, [R i, A i]_[𝓟 S]) × Y` (with `S` cofinite) is continuous. -/
theorem continuous_dom_prod_right {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
{f : Πʳ i, [R i, A i] × Y → X} :
Continuous f ↔ ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous (f ∘ (Prod.map (inclusion R A hS) id)) :=
by
refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id), fun H ↦ ?_⟩
simp_rw [continuous_iff_continuousAt, ContinuousAt]
rintro ⟨x, y⟩
set S : Set ι := {i | x i ∈ A i}
have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr x.2
have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩
rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x', ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ←
nhds_prod_eq, tendsto_map'_iff]
exact
H S hS |>.tendsto
⟨x', y⟩
-- TODO: get from the previous one instead of copy-pasting
