tendsto_prod_uniformity_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem tendsto_prod_uniformity_fst [UniformSpace α] [UniformSpace β] :
    Tendsto (fun p : (α × β) × α × β => (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α) :=
  le_trans (map_mono inf_le_left) map_comap_le

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