uniformity_prod — Mathlib

English

A HasBasis description for the uniformity of a product is given by combining the bases of the factors via entourageProd.

Русский

Описание униформности произведения через базисные множества факторов с помощью entourageProd.

LaTeX

$$$(\text{Filter.HasBasis.uniformity_prod}) : (\mathcal{U}(\alpha))\.HasBasis \,...\to\ (\mathcal{U}(\alpha \times \beta)).HasBasis$$$

Lean4

theorem uniformity_prod {ιa ιb : Type*} [UniformSpace α] [UniformSpace β] {pa : ιa → Prop} {pb : ιb → Prop}
    {sa : ιa → Set (α × α)} {sb : ιb → Set (β × β)} (ha : (𝓤 α).HasBasis pa sa) (hb : (𝓤 β).HasBasis pb sb) :
    (𝓤 (α × β)).HasBasis (fun i : ιa × ιb ↦ pa i.1 ∧ pb i.2) (fun i ↦ entourageProd (sa i.1) (sb i.2)) :=
  (ha.comap _).inf (hb.comap _)

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