prod — Mathlib

English

If e1 and e2 are uniform inducing, then their product map (e1, e2) is uniform inducing.

Русский

Если e1 и e2 UniformInducing, то их произведение (e1, e2) равно UniformInducing.

LaTeX

$$$IsUniformInducing e_1 \\to e_2 \\Rightarrow IsUniformInducing (\\lambda p: (e_1 p.1, e_2 p.2))$$$

Lean4

theorem prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'}
    (h₁ : IsUniformInducing e₁) (h₂ : IsUniformInducing e₂) : IsUniformInducing fun p : α × β => (e₁ p.1, e₂ p.2) :=
  ⟨by simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]⟩

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