isUltrametricDist — Mathlib

English

Continuous maps from a compact space to an ultrametric space form an ultrametric space with the sup metric.

Русский

Непрерывные отображения из компактного пространства в ультраметрическое образуют ультраметрическое пространство при метрике по максимуму (супметрике).

LaTeX

$$IsUltrametricDist C(X,Y)$$

Lean4

/-- Continuous maps from a compact space to an ultrametric space are an ultrametric space. -/
instance isUltrametricDist {X Y : Type*} [TopologicalSpace X] [CompactSpace X] [MetricSpace Y] [IsUltrametricDist Y] :
    IsUltrametricDist C(X, Y) := by
  constructor
  intro f g h
  rw [ContinuousMap.dist_le (by positivity)]
  refine fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_) <;>
    exact ContinuousMap.dist_apply_le_dist x

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