entourageProd_mem_uniformity — Mathlib

English

If u ∈ 𝓤 α and v ∈ 𝓤 β, then entourageProd u v ∈ 𝓤 (α × β).

Русский

Если u ∈ 𝓤 α и v ∈ 𝓤 β, то entourageProd u v ∈ 𝓤 (α × β).

LaTeX

$$$u \in 𝓤(\alpha) \land v \in 𝓤(\beta) \Rightarrow \text{entourageProd}(u,v) \in 𝓤(\alpha \times \beta)$$$

Lean4

theorem entourageProd_mem_uniformity [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : Set (α × α)} {v : Set (β × β)}
    (hu : u ∈ 𝓤 α) (hv : v ∈ 𝓤 β) : entourageProd u v ∈ 𝓤 (α × β) := by rw [uniformity_prod];
  exact inter_mem_inf (preimage_mem_comap hu) (preimage_mem_comap hv)

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