English
Let t: ι → Set α be a nonempty directed subfamily of 𝔖 with hex ensuring coverage. If V is a basis for 𝓤 β, then UniformOnFun.gen 𝔖 (t_i) (V_j) with i, j as indices gives a basis for 𝓤(α →ᵤ[𝔖] β).
Русский
Пусть t — направленная непустая подпоследовательность 𝔖, которая покрывает 𝔖; если V — база 𝓤 β, то UniformOnFun.gen 𝔖 (t_i) (V_j) образует базис равномерности на α→ᵤ[𝔖]β.
LaTeX
$$$\text{If } ht : \forall i, t(i)∈ 𝔖,\; hdir: Directed,\; hex: ∀ s∈𝔖, ∃ i, s ⊆ t(i), \; hb: HasBasis (𝓤 β) p V,\; then\ (𝓤(α→ᵤ[𝔖]β)).HasBasis (fun i => p i.2) (fun i => UniformOnFun.gen 𝔖 (t i.1) (V i.2)).$$$
Lean4
/-- Let `t i` be a nonempty directed subfamily of `𝔖`
such that every `s ∈ 𝔖` is included in some `t i`.
Let `V` bounded by `p` be a basis of entourages of `β`.
Then `UniformOnFun.gen 𝔖 (t i) (V j)` bounded by `p j` is a basis of entourages of `α →ᵤ[𝔖] β`. -/
protected theorem hasBasis_uniformity_of_covering_of_basis {ι ι' : Type*} [Nonempty ι] {t : ι → Set α} {p : ι' → Prop}
{V : ι' → Set (β × β)} (ht : ∀ i, t i ∈ 𝔖) (hdir : Directed (· ⊆ ·) t) (hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i)
(hb : HasBasis (𝓤 β) p V) :
(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i : ι × ι' ↦ p i.2) fun i ↦ UniformOnFun.gen 𝔖 (t i.1) (V i.2) :=
by
have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦
by
rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
refine
(UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_)
fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩
rcases hex s hs with ⟨i, hi⟩
exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩
