English
A finitary version of the continuous_dom theorem: for a finite index set n, a map on a product of restricted products is continuous iff its coordinatewise inclusions are continuous.
Русский
Финитное аналоги к теореме: отображение непрерывно тогда и только тогда, когда каждое координатное включение непрерывно.
LaTeX
$$$\\forall \\;\\text{finite } n, \\; \\text{Continuous}(f) \\iff \\forall S, hS, \\text{Continuous}(f \\circ \\text{Pi.map} \\;\\langle \\text{inclusions}\\rangle)$$$
Lean4
/-- A map from `Πʳ i, [R i, A i] × Πʳ i, [R' i, A' i]` is continuous
*iff* its restriction to each `Πʳ i, [R i, A i]_[𝓟 S] × Πʳ i, [R' i, A' i]_[𝓟 S]`
(with `S` cofinite) is continuous.
This is the key result for continuity of multiplication and addition. -/
theorem continuous_dom_prod {R' : ι → Type*} {A' : (i : ι) → Set (R' i)} [∀ i, TopologicalSpace (R' i)]
(hAopen' : ∀ i, IsOpen (A' i)) {X : Type*} [TopologicalSpace X] {f : Πʳ i, [R i, A i] × Πʳ i, [R' i, A' i] → X} :
Continuous f ↔
∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous (f ∘ (Prod.map (inclusion R A hS) (inclusion R' A' hS))) :=
by
simp_rw [continuous_dom_prod_right hAopen, continuous_dom_prod_left hAopen']
refine ⟨fun H S hS ↦ H S hS S hS, fun H S hS T hT ↦ ?_⟩
set U := S ∩ T
have hU : cofinite ≤ 𝓟 (S ∩ T) := inf_principal ▸ le_inf hS hT
have hSU : 𝓟 U ≤ 𝓟 S := principal_mono.mpr inter_subset_left
have hTU : 𝓟 U ≤ 𝓟 T := principal_mono.mpr inter_subset_right
exact (H U hU).comp ((continuous_inclusion hSU).prodMap (continuous_inclusion hTU))
