English
Defines a premeteric space structure on Σ n, X_n with dist = inductiveLimitDist and standard metric-space symmetry/triangle properties.
Русский
Задает структуру предметрического пространства на Σ_n X_n с расстоянием, заданным inductiveLimitDist, и сохраняет симметрию/неравенство треугольника.
LaTeX
$$$\text{inductivePremetric}(I) :\text{PseudoMetricSpace}(\Sigma n, X_n)\quad\text{with}\quad\mathrm{dist}=\mathrm{inductiveLimitDist} f$$$
Lean4
/-- Premetric space structure on `Σ n, X n`. -/
def inductivePremetric (I : ∀ n, Isometry (f n)) : PseudoMetricSpace (Σ n, X n)
where
dist := inductiveLimitDist f
dist_self x := by simp [inductiveLimitDist]
dist_comm x
y := by
let m := max x.1 y.1
have hx : x.1 ≤ m := le_max_left _ _
have hy : y.1 ≤ m := le_max_right _ _
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx, dist_comm]
dist_triangle x y
z := by
let m := max (max x.1 y.1) z.1
have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _)
have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _)
have hz : z.1 ≤ m := le_max_right _ _
calc
inductiveLimitDist f x z = dist (leRecOn hx (f _) x.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
inductiveLimitDist_eq_dist I x z m hx hz
_ ≤
dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m) +
dist (leRecOn hy (f _) y.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
(dist_triangle _ _ _)
_ = inductiveLimitDist f x y + inductiveLimitDist f y z := by
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
