prod — Mathlib

English

If e1 and e2 are uniform embeddings, then the map p ↦ (e1 p.1, e2 p.2) is a uniform embedding on the product.

Русский

Если e1 и e2 — равномерные вложения, то отображение на произведении является равномерным вложением.

LaTeX

$$$\\text{IsUniformEmbedding}(\\lambda p: α×β \\mapsto (e1 p.1, e2 p.2))$$$

Lean4

theorem prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'}
    (h₁ : IsUniformEmbedding e₁) (h₂ : IsUniformEmbedding e₂) : IsUniformEmbedding fun p : α × β => (e₁ p.1, e₂ p.2)
    where
  toIsUniformInducing := h₁.isUniformInducing.prod h₂.isUniformInducing
  injective := h₁.injective.prodMap h₂.injective

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