basis_uniformity — Mathlib

English

If f is IsUniformInducing and H is a basis for the uniformity on β, then the uniformity on α has a corresponding basis pulled back via Prod.map f f.

Русский

Если f — IsUniformInducing, и H — база для равномерности β, то равномерность α имеет соответствующую базу через отображение Prod.map f f.

LaTeX

$$$\\text{basis_uniformity}$$$

Lean4

theorem basis_uniformity {f : α → β} (hf : IsUniformInducing f) {ι : Sort*} {p : ι → Prop} {s : ι → Set (β × β)}
    (H : (𝓤 β).HasBasis p s) : (𝓤 α).HasBasis p fun i => Prod.map f f ⁻¹' s i :=
  hf.1 ▸ H.comap _

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