English
Bourbaki GT III.6.5 Theorem I: Bilinear maps defined on dense images into a complete Hausdorff group extend continuously.
Русский
Теорема Бурбаки о непрерывном продолжении билинейной карты, определённой на плотных образах, в полную точную группу.
LaTeX
$$$\text{ExtendZBilin}$: Continuous extension of a bilinear map from dense images to a complete Hausdorff group.$$
Lean4
/-- Bourbaki GT III.6.5 Theorem I:
ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary. -/
theorem extend_Z_bilin : Continuous (extend (de.prodMap df) (fun p : β × δ => φ p.1 p.2)) :=
by
refine continuous_extend_of_cauchy _ ?_
rintro ⟨x₀, y₀⟩
constructor
· apply NeBot.map
apply comap_neBot
intro U h
rcases mem_closure_iff_nhds.1 ((de.prodMap df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩
exists z
simp_all
· suffices
map (fun p : (β × δ) × β × δ => (fun p : β × δ => φ p.1 p.2) p.2 - (fun p : β × δ => φ p.1 p.2) p.1)
(comap (fun p : (β × δ) × β × δ => ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2))) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
𝓝 0
by
rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map, prod_comap_comap_eq]
intro W' W'_nhds
have key := extend_Z_bilin_key de df hφ W'_nhds x₀ y₀
rcases key with ⟨U, U_nhds, V, V_nhds, h⟩
rw [mem_comap] at U_nhds
rcases U_nhds with ⟨U', U'_nhds, U'_sub⟩
rw [mem_comap] at V_nhds
rcases V_nhds with ⟨V', V'_nhds, V'_sub⟩
rw [mem_map, mem_comap, nhds_prod_eq]
exists (U' ×ˢ V') ×ˢ U' ×ˢ V'
rw [mem_prod_same_iff]
have := prod_mem_prod U'_nhds V'_nhds
grind
