English
A universal property of the restricted product topology: a map from the restricted product to a space X is continuous if and only if its restrictions to all principal subproducts are continuous.
Русский
Универсальная свойство топологии ограниченного произведения: отображение из ограниченного произведения в X непрерывно тогда и только тогда, когда его ограничения на все подпроизведения по принципу непрерывны.
LaTeX
$$$\\text{Continuous } f \\iff \\forall (S : Set ι) (hS : 𝓕 \\le 𝓟 S), \\ \\text{Continuous}(f \\circ \\iota_{R,A,hS})$$$
Lean4
/-- The **universal property** of the topology on the restricted product: a map from
`Πʳ i, [R i, A i]_[𝓕]` is continuous *iff* its restriction to each `Πʳ i, [R i, A i]_[𝓟 s]`
(with `𝓕 ≤ 𝓟 s`) is continuous.
See also `RestrictedProduct.continuous_dom_prod_left`. -/
theorem continuous_dom {X : Type*} [TopologicalSpace X] {f : Πʳ i, [R i, A i]_[𝓕] → X} :
Continuous f ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous (f ∘ inclusion R A hS) := by
simp_rw [topologicalSpace_eq_of_principal, continuous_iSup_dom, continuous_coinduced_dom]
