English
A binary product of proper maps is proper.
Русский
Двоичное произведение правильных отображений корректно.
LaTeX
$$$IsProperMap f \land IsProperMap g \Rightarrow IsProperMap (Prod.map f g)$$$
Lean4
/-- A binary product of proper maps is proper. -/
theorem prodMap {g : Z → W} (hf : IsProperMap f) (hg : IsProperMap g) : IsProperMap (Prod.map f g) :=
by
simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢
constructor
-- Continuity is clear.
·
exact
hf.1.prodMap
hg.1
-- Let `𝒰 : Ultrafilter (X × Z)`, and assume that `f × g` tends to some `(y, w) : Y × W`
-- along `𝒰`.
· intro 𝒰 ⟨y, w⟩ hyw
simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw
rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using hyw.1) with ⟨x, hxy, hx⟩
rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using hyw.2) with
⟨z, hzw, hz⟩
-- By the properties of the product topology, that means that `𝒰` tends to `(x, z)`,
-- which completes the proof since `(f × g)(x, z) = (y, w)`.
refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
rw [nhds_prod_eq, le_prod]
exact ⟨hx, hz⟩
