uniformCore — Mathlib

Lean4
/-- Core of the uniform structure of uniform convergence. -/
protected def uniformCore : UniformSpace.Core (α →ᵤ β) :=
  UniformSpace.Core.mkOfBasis (UniformFun.basis α β (𝓤 β))
    (fun _ ⟨_, hV, hVU⟩ _ => hVU ▸ fun _ => refl_mem_uniformity hV)
    (fun _ ⟨V, hV, hVU⟩ =>
      hVU ▸
        ⟨UniformFun.gen α β (Prod.swap ⁻¹' V), ⟨Prod.swap ⁻¹' V, tendsto_swap_uniformity hV, rfl⟩, fun _ huv x =>
          huv x⟩)
    fun _ ⟨_, hV, hVU⟩ =>
    hVU ▸
      let ⟨W, hW, hWV⟩ := comp_mem_uniformity_sets hV
      ⟨UniformFun.gen α β W, ⟨W, hW, rfl⟩, fun _ ⟨w, huw, hwv⟩ x => hWV ⟨w x, ⟨huw x, hwv x⟩⟩⟩
Похожие утверждения