instPseudoMetricSpaceOfBoundedSpace

English

If β has a bounded space structure, then UniformOnFun α 𝔖 β carries a natural pseudometric coming from the sup-distance over ⋃𝔖.

Русский

Если β имеет ограниченное пространство, то UniformOnFun α 𝔖 β оснащается естественной псевдометрической структурой, заданной как супримум расстояний по ⋃𝔖.

LaTeX

$$$\text{If } \text{BoundedSpace}(\beta) \text{ then } \text{PseudoMetricSpace}(\alpha \to_{\mathfrak{S}} \beta)$ with $d(f,g) = \sup_{x \in ⋃𝔖} \operatorname{dist}(f(x), g(x)).$$$

Lean4

noncomputable instance [BoundedSpace β] : PseudoMetricSpace (α →ᵤ[𝔖] β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ⨆ x ∈ ⋃₀ 𝔖, dist (toFun 𝔖 f x) (toFun 𝔖 g x))
    (fun _ _ ↦ by
      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
      exact (iSup₂_le fun x _ ↦ EMetric.edist_le_diam_of_mem (Set.mem_univ _) (Set.mem_univ _)) |>.trans_lt this |>.ne)
    (fun _ _ ↦ by
      simp only [dist_edist, edist_def, ← ENNReal.toReal_iSup (fun _ ↦ edist_ne_top _ _)]
      rw [ENNReal.toReal_iSup]
      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
      refine fun x ↦ lt_of_le_of_lt (iSup_le fun hx ↦ ?_) this |>.ne
      exact EMetric.edist_le_diam_of_mem (Set.mem_univ _) (Set.mem_univ _))

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