tendsto_prod_uniformity_snd — Mathlib

English

The projection from the product uniformity to the second coordinate uniformity is continuous.

Русский

Пределение проекции из униформности произведения на униформность второй координаты соответствует непрерывности.

LaTeX

$$$\mathrm{Tendsto\} \big( (p_1, p_2) \mapsto p_2 \big) \; (\mathcal{U}(\alpha \times \beta)) \; (\mathcal{U}(\beta))$$$

Lean4

theorem tendsto_prod_uniformity_snd [UniformSpace α] [UniformSpace β] :
    Tendsto (fun p : (α × β) × α × β => (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β) :=
  le_trans (map_mono inf_le_right) map_comap_le

Похожие утверждения