English
A product map over an index set is proper if each component is proper.
Русский
Произведение отображений по индексному множеству проперно, если каждый компонент проперен.
LaTeX
$$$\forall i, IsProperMap (f i) \Rightarrow IsProperMap (\lambda x i, f i (x i))$$$
Lean4
/-- Any product of proper maps is proper. -/
theorem pi_map {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i}
(h : ∀ i, IsProperMap (f i)) : IsProperMap (fun (x : ∀ i, X i) i ↦ f i (x i)) :=
by
simp_rw [isProperMap_iff_ultrafilter] at h ⊢
constructor
-- Continuity is clear.
·
exact
continuous_pi fun i ↦
(h i).1.comp
(continuous_apply i)
-- Let `𝒰 : Ultrafilter (Π i, X i)`, and assume that `Π i, f i` tends to some `y : Π i, Y i`
-- along `𝒰`.
· intro 𝒰 y hy
have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by simpa [tendsto_pi_nhds] using hy
choose x hxy hx using fun i ↦
(h i).2
(this i)
-- By the properties of the product topology, that means that `𝒰` tends to `x`,
-- which completes the proof since `(Π i, f i) x = y`.
refine ⟨x, funext hxy, ?_⟩
rwa [nhds_pi, le_pi]
