English
If 𝔖 is nonempty and directed, and 𝓑 is a basis for the entourages of β, then the family UniformOnFun.gen 𝔖 S V (with S ∈ 𝔖 and V ∈ 𝓑) forms a basis for the product uniformity on (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β).
Русский
Если 𝔖 не пусто и ориентировано, и 𝓑 — база околодности β, то семейство UniformOnFun.gen 𝔖 S V (S∈𝔖, V∈𝓑) образует базис для произведения равномерности на (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β).
LaTeX
$$$\text{If } 𝔖\neq \varnothing,\; 𝔖 \text{ is directed, and } 𝓑 \text{ is a basis for } 𝓤(β), \text{ then }\{\mathrm{UniformOnFun.gen}\ 𝔖 S V : S\in 𝔖, V\in 𝓑\}$ is a basis for $\mathcal U((α→ᵤ[𝔖]β)\times(α→ᵤ[𝔖]β))$.$$
Lean4
/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis on `β × β`, then the
family `UniformOnFun.gen 𝔖 S V` for `S ∈ 𝔖` and `V ∈ 𝓑` is a filter basis on
`(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)`.
We will show in `has_basis_uniformity_of_basis` that, if `𝓑` is a basis for `𝓤 β`, then the
corresponding filter is the uniformity of `α →ᵤ[𝔖] β`. -/
protected theorem isBasis_gen (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖)
(𝓑 : FilterBasis <| β × β) :
IsBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2 :=
⟨h.prod 𝓑.nonempty, fun {U₁V₁ U₂V₂} h₁ h₂ =>
let ⟨U₃, hU₃, hU₁₃, hU₂₃⟩ := h' U₁V₁.1 h₁.1 U₂V₂.1 h₂.1
let ⟨V₃, hV₃, hV₁₂₃⟩ := 𝓑.inter_sets h₁.2 h₂.2
⟨⟨U₃, V₃⟩,
⟨⟨hU₃, hV₃⟩, fun _ H => ⟨fun x hx => (hV₁₂₃ <| H x <| hU₁₃ hx).1, fun x hx => (hV₁₂₃ <| H x <| hU₂₃ hx).2⟩⟩⟩⟩
