entourageProd_subset — Mathlib

English

Every entourage of α × β contains a basic entourageProd of some entourages in α and β.

Русский

Каждое окружение пространства α × β содержит базовое окружениеProd некоторых окружений в α и β.

LaTeX

$$$\exists u \in 𝓤(\alpha), \exists v \in 𝓤(\beta), entourageProd(u,v) \subseteq s$$$

Lean4

theorem entourageProd_subset [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)} (h : s ∈ 𝓤 (α × β)) :
    ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s :=
  by
  rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩
  use w.1, hw.1.1, w.2, hw.1.2, hw.2

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