English
A dual universal property with parameters for the left-hand restricted product product with Y as parameter: a map is continuous iff its precomposed with the left inclusion is continuous.
Русский
Аналогично слева: отображение непрерывно тогда и только тогда, когда его проскалирование по левому включению непрерывно.
LaTeX
$$$\\text{Continuous f} \\iff \\forall S, hS, \\text{Continuous}(f \\circ (\\text{Prod.map} \\text{id (inclusion R A hS)}))$$$
Lean4
/-- The **universal property with parameters** of the topology on the restricted product:
for any topological space `Y` of "parameters", a map from `Y × Πʳ i, [R i, A i]` is continuous
*iff* its restriction to each `Y × Πʳ i, [R i, A i]_[𝓟 S]` (with `S` cofinite) is continuous. -/
theorem continuous_dom_prod_left {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
{f : Y × Πʳ i, [R i, A i] → X} :
Continuous f ↔ ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous (f ∘ (Prod.map id (inclusion R A hS))) :=
by
refine ⟨fun H S hS ↦ H.comp (continuous_id.prodMap (continuous_inclusion hS)), fun H ↦ ?_⟩
simp_rw [continuous_iff_continuousAt, ContinuousAt]
rintro ⟨y, x⟩
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 ⟨y, x'⟩
