hasBasis_uniformity_of_basis_aux₁

English

If 𝔖 has a basis for 𝓤 β, then the uniformity on α →ᵤ[𝔖] β has a basis given by UniformOnFun.gen 𝔖 S (s i) for S ∈ 𝔖 and i in the index set.

Русский

Если у 𝔖 есть база равномерности β, то равномерность на α →ᵤ[𝔖] β имеет базис, задаваемый UniformOnFun.gen 𝔖 S (s i).

LaTeX

$$$\text{If } hb: \text{HasBasis }(\mathcal U β)\ p\ i \text{ and } S\in 𝔖,\; (s_i) \\text{ then } (\mathcal U(α→ᵤ[𝔖]β)).HasBasis p\ i\mapsto UniformOnFun.gen 𝔖 S (s i).$$$

Lean4

protected theorem hasBasis_uniformity_of_basis_aux₁ {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s)
    (S : Set α) :
    (@uniformity (α →ᵤ[𝔖] β) ((UniformFun.uniformSpace S β).comap S.restrict)).HasBasis p fun i =>
      UniformOnFun.gen 𝔖 S (s i) :=
  by
  simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]
  exact (UniformFun.hasBasis_uniformity_of_basis S β hb).comap _

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