English
A restatement of the previous covering basis lemma, giving the same conclusion under the same hypotheses.
Русский
Переформулировка предыдущей леммы о базисе покрытия.
LaTeX
$$$\text{(same as above): } (𝓤(α→ᵤ[𝔖]β))\HasBasis ...$$$
Lean4
/-- If `t n` is a monotone sequence of sets in `𝔖`
such that each `s ∈ 𝔖` is included in some `t n`
and `V n` is an antitone basis of entourages of `β`,
then `UniformOnFun.gen 𝔖 (t n) (V n)` is an antitone basis of entourages of `α →ᵤ[𝔖] β`. -/
protected theorem hasAntitoneBasis_uniformity {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {t : ι → Set α}
{V : ι → Set (β × β)} (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n)
(hb : HasAntitoneBasis (𝓤 β) V) : (𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n) :=
by
have := hb.nonempty
refine
⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖 ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦
⟨(i, i), trivial, Subset.rfl⟩,
?_⟩
· rintro ⟨k, l⟩ -
rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩
exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩
· exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)
