isUniformInducing_equivBoundedOfCompact

English

Let α be a compact space and β a metric space. The natural identification between continuous maps C(α, β) and bounded continuous maps α →ᵇ β is uniform-inducing; in particular, the uniform structure on C(α, β) is obtained by pulling back the uniform structure from α →ᵇ β along the canonical Equivalence given by equivBoundedOfCompact.

Русский

Пусть α—компактное пространство и β—метрическое пространство. Естественное отображение между непрерывными отображениями C(α, β) и ограниченными непрерывными отображениями α →ᵇ β является равномерно индуцирующим; другими словами, равномерная структура пространства C(α, β) получается как вытяжка из структуры α →ᵇ β по каноническому гомоморфизму, заданному эквивалентностью equivBoundedOfCompact.

LaTeX

$$$\mathrm{IsUniformInducing}\bigl(\mathrm{equivBoundedOfCompact}(\alpha,\beta)\bigr)$$$

Lean4

theorem isUniformInducing_equivBoundedOfCompact : IsUniformInducing (equivBoundedOfCompact α β) :=
  IsUniformInducing.mk'
    (by
      simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
      exact fun s =>
        ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
          ⟨{p | ∀ x, (p.1 x, p.2 x) ∈ b}, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩, fun f g h =>
            hs fun x _ => h x⟩,
          fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
          ⟨⟨Set.univ, {p | dist p.1 p.2 ≤ ε}⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩, fun ⟨f, g⟩ h =>
            hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩)

Похожие утверждения