English
The topological space UniformOnFun.topologicalSpace α β 𝔖 equals the infimum over S ∈ 𝔖 of the induced topologies via the restriction map to S.
Русский
Топологическое пространство UniformOnFun.topologicalSpace α β 𝔖 равно пересечению (инфинуму) топологий, индуцируемых ограничением на каждый S ∈ 𝔖.
LaTeX
$$$\ UniformOnFun.topologicalSpace\ α\ β\ 𝔖 = \bigwedge_{S∈𝔖} \mathrm{TopologicalSpace.induced}(\mathrm{UniformFun.ofFun} \circ S.restrict \circ \mathrm{toFun} 𝔖)
(\mathrm UniformFun.topologicalSpace\ S\ β).$$$
Lean4
/-- The topology of `𝔖`-convergence is the infimum, for `S ∈ 𝔖`, of topology induced by the map
of `S.restrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β)` of restriction to `S`, where `↥S →ᵤ β` is endowed with
the topology of uniform convergence. -/
protected theorem topologicalSpace_eq :
UniformOnFun.topologicalSpace α β 𝔖 =
⨅ (s : Set α) (_ : s ∈ 𝔖),
TopologicalSpace.induced (UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖) (UniformFun.topologicalSpace s β) :=
by
simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]
rfl
