English
If {U_i} is a basis of entourages on X, then the entourages for Path x y defined by ∀ t, (γ1 t, γ2 t) ∈ U_i form a basis on Path x y.
Русский
Если {U_i} — база окружностей на X, то окружения для Path x y, определяемые по ∀ t, (γ1 t, γ2 t) ∈ U_i, образуют базис на Path x y.
LaTeX
$$$\text{HasBasis } 𝓤(\mathrm{Path}(x,y))\ (p_i)\ { γ\,|\, ∀t, (γ_1(t), γ_2(t)) ∈ U_i }$$$
Lean4
/-- If `{U i | p i}` form a basis of entourages of `X`,
then the entourages `{V i | p i}`, `V i = {(γ₁, γ₂) | ∀ t, (γ₁ t, γ₂ t) ∈ U i}`,
form a basis of entourages of paths between `x` and `y`. -/
theorem _root_.Filter.HasBasis.uniformityPath {ι : Sort*} {p : ι → Prop} {U : ι → Set (X × X)}
(hU : (𝓤 X).HasBasis p U) : (𝓤 (Path x y)).HasBasis p fun i ↦ {γ | ∀ t, (γ.1 t, γ.2 t) ∈ U i} :=
hU.compactConvergenceUniformity_of_compact.comap _
